src/HOL/Divides.thy
changeset 63417 c184ec919c70
parent 63317 ca187a9f66da
child 63499 9c9a59949887
     1.1 --- a/src/HOL/Divides.thy	Fri Jul 08 23:43:11 2016 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sat Jul 09 13:26:16 2016 +0200
     1.3 @@ -1432,6 +1432,15 @@
     1.4    apply (metis (full_types) One_nat_def Suc_lessI div_less_dividend less_not_refl3)
     1.5    done
     1.6  
     1.7 +lemma (in field_char_0) of_nat_div:
     1.8 +  "of_nat (m div n) = ((of_nat m - of_nat (m mod n)) / of_nat n)"
     1.9 +proof -
    1.10 +  have "of_nat (m div n) = ((of_nat (m div n * n + m mod n) - of_nat (m mod n)) / of_nat n :: 'a)"
    1.11 +    unfolding of_nat_add by (cases "n = 0") simp_all
    1.12 +  then show ?thesis
    1.13 +    by simp
    1.14 +qed
    1.15 +
    1.16  
    1.17  subsubsection \<open>An ``induction'' law for modulus arithmetic.\<close>
    1.18