diff options
| author | letouzey | 2010-01-05 15:24:38 +0000 |
|---|---|---|
| committer | letouzey | 2010-01-05 15:24:38 +0000 |
| commit | 41138b8f14d17f3c409d592c18e5a4def664a2e8 (patch) | |
| tree | 53e61dcd72940f85a085c51d5dc579ffa84a0d86 /theories/Numbers/Integer/Abstract | |
| parent | f4ceaf2ce34c5cec168275dee3e7a99710bf835f (diff) | |
Avoid declaring hints about refl/sym/trans of eq in DecidableType2
This used to be convenient in FSets, but since we now try to integrate
DecidableType and OrderedType as foundation for other part of the stdlib,
this should be avoided, otherwise some eauto take a _long_ time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
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. |