summaryrefslogtreecommitdiff
path: root/theories/ZArith/Znat.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/Znat.v')
-rw-r--r--theories/ZArith/Znat.v37
1 files changed, 19 insertions, 18 deletions
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index c5b5edc1..dfd9b545 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Znat.v 10726 2008-03-28 18:15:23Z notin $ i*)
+(*i $Id$ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
@@ -57,15 +58,15 @@ Proof.
| discriminate H0
| discriminate H0
| simpl in H0; injection H0;
- do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ;
+ do 2 rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ;
intros E; rewrite E; auto with arith ].
-Qed.
+Qed.
Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
Proof.
intros x y H.
destruct (eq_nat_dec x y) as [H'|H']; auto.
- elimtype False.
+ exfalso.
exact (inj_neq _ _ H' H).
Qed.
@@ -90,7 +91,7 @@ Qed.
Theorem inj_lt : forall n m:nat, (n < m)%nat -> Z_of_nat n < Z_of_nat m.
Proof.
- intros x y H; apply Zgt_lt; apply Zlt_succ_gt; rewrite <- inj_S; apply inj_le;
+ intros x y H; apply Zgt_lt; apply Zle_succ_gt; rewrite <- inj_S; apply inj_le;
exact H.
Qed.
@@ -110,7 +111,7 @@ Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
Proof.
intros x y H.
destruct (le_lt_dec x y) as [H0|H0]; auto.
- elimtype False.
+ exfalso.
assert (H1:=inj_lt _ _ H0).
red in H; red in H1.
rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
@@ -120,7 +121,7 @@ Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
Proof.
intros x y H.
destruct (le_lt_dec y x) as [H0|H0]; auto.
- elimtype False.
+ exfalso.
assert (H1:=inj_le _ _ H0).
red in H; red in H1.
rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
@@ -130,7 +131,7 @@ Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
Proof.
intros x y H.
destruct (le_lt_dec y x) as [H0|H0]; auto.
- elimtype False.
+ exfalso.
assert (H1:=inj_gt _ _ H0).
red in H; red in H1.
rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
@@ -140,7 +141,7 @@ Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
Proof.
intros x y H.
destruct (le_lt_dec x y) as [H0|H0]; auto.
- elimtype False.
+ exfalso.
assert (H1:=inj_ge _ _ H0).
red in H; red in H1.
rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
@@ -169,7 +170,7 @@ Proof.
Qed.
(** Injection and usual operations *)
-
+
Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
Proof.
intro x; induction x as [| n H]; intro y; destruct y as [| m];
@@ -186,7 +187,7 @@ Proof.
intro x; induction x as [| n H];
[ simpl in |- *; trivial with arith
| intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
- rewrite <- inj_plus; simpl in |- *; rewrite plus_comm;
+ rewrite <- inj_plus; simpl in |- *; rewrite plus_comm;
trivial with arith ].
Qed.
@@ -195,17 +196,17 @@ Theorem inj_minus1 :
Proof.
intros x y H; apply (Zplus_reg_l (Z_of_nat y)); unfold Zminus in |- *;
rewrite Zplus_permute; rewrite Zplus_opp_r; rewrite <- inj_plus;
- rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r;
+ rewrite <- (le_plus_minus y x H); rewrite Zplus_0_r;
trivial with arith.
Qed.
-
+
Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z_of_nat (n - m) = 0.
Proof.
intros x y H; rewrite not_le_minus_0;
[ trivial with arith | apply gt_not_le; assumption ].
Qed.
-Theorem inj_minus : forall n m:nat,
+Theorem inj_minus : forall n m:nat,
Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
Proof.
intros.
@@ -225,7 +226,7 @@ Proof.
unfold Zminus; rewrite H'; auto.
Qed.
-Theorem inj_min : forall n m:nat,
+Theorem inj_min : forall n m:nat,
Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
Proof.
induction n; destruct m; try (compute; auto; fail).
@@ -234,7 +235,7 @@ Proof.
rewrite <- Zsucc_min_distr; f_equal; auto.
Qed.
-Theorem inj_max : forall n m:nat,
+Theorem inj_max : forall n m:nat,
Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
Proof.
induction n; destruct m; try (compute; auto; fail).
@@ -269,11 +270,11 @@ Proof.
intros x; exists (Z_of_nat x); split;
[ trivial with arith
| rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
- unfold Zle in |- *; elim x; intros; simpl in |- *;
+ unfold Zle in |- *; elim x; intros; simpl in |- *;
discriminate ].
Qed.
-Lemma Zpos_P_of_succ_nat : forall n:nat,
+Lemma Zpos_P_of_succ_nat : forall n:nat,
Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
Proof.
intros.