diff options
Diffstat (limited to 'theories/Ints/Z')
| -rw-r--r-- | theories/Ints/Z/IntsZmisc.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Ints/Z/IntsZmisc.v b/theories/Ints/Z/IntsZmisc.v index 6fcaaa6e9f..e4dee2d4f6 100644 --- a/theories/Ints/Z/IntsZmisc.v +++ b/theories/Ints/Z/IntsZmisc.v @@ -100,7 +100,7 @@ Definition is_lt (n m : positive) := end. Infix "?<" := is_lt (at level 70, no associativity) : P_scope. -Lemma is_lt_spec : forall n m, if n ?< m then n < m else m <= n. +Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z. Proof. intros n m; unfold is_lt, Zlt, Zle, Zcompare. rewrite (ZC4 m n);destruct ((n ?= m) Eq);trivial;try (intro;discriminate). |