diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 15b8a9cd02..b57f8e27fb 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -498,6 +498,7 @@ Theorem add_mod: forall a b n, n~=0 -> 0 <= a*b -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. intros a b n Hn Hab. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. +reflexivity. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]; destruct (le_0_mul _ _ (mod_sign b n Hn)) as [(Hb',Hm)|(Hb',Hm)]; auto using mul_nonneg_nonneg, mul_nonpos_nonpos. |