summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zeven.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Zeven.v')
-rw-r--r--theories/ZArith/Zeven.v8
1 files changed, 5 insertions, 3 deletions
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index c83a863f..d88bf7a9 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -197,12 +197,14 @@ Qed.
Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2.
Proof.
assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2).
- { intros m Hm.
+ {
+ intros m Hm.
apply Z.quot_unique with (if Z.odd m then Z.sgn m else 0).
now apply Z.lt_le_incl.
rewrite Z.sgn_pos by trivial.
destruct (Z.odd m); now split.
- apply Zquot2_odd_eqn. }
+ apply Zquot2_odd_eqn.
+ }
destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]].
- now apply AUX.
- now subst.