equal
deleted
inserted
replaced
525 |
525 |
526 instantiation nat :: semiring_div |
526 instantiation nat :: semiring_div |
527 begin |
527 begin |
528 |
528 |
529 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where |
529 definition divmod_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat" where |
530 [code del]: "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)" |
530 "divmod_nat m n = (THE qr. divmod_nat_rel m n qr)" |
531 |
531 |
532 lemma divmod_nat_rel_divmod_nat: |
532 lemma divmod_nat_rel_divmod_nat: |
533 "divmod_nat_rel m n (divmod_nat m n)" |
533 "divmod_nat_rel m n (divmod_nat m n)" |
534 proof - |
534 proof - |
535 from divmod_nat_rel_ex |
535 from divmod_nat_rel_ex |