aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zmax.v
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-10-17 12:53:34 +0000
commit28dc7a05cc1d3e03ed1435b3db4340db954a59e2 (patch)
tree63cdf18cd47260eb90550f62f7b22e2e2e208f6c /theories/ZArith/Zmax.v
parent744e7f6a319f4d459a3cc2309f575d43041d75aa (diff)
Mise en forme des theories
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zmax.v')
-rw-r--r--theories/ZArith/Zmax.v58
1 files changed, 29 insertions, 29 deletions
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 4f6251551..ca647ff3c 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -14,95 +14,95 @@ Require Import Zorder.
Open Local Scope Z_scope.
-(**********************************************************************)
-(** *** Maximum of two binary integer numbers *)
+(******************************************)
+(** Maximum of two binary integer numbers *)
Definition Zmax m n :=
- match m ?= n with
+ match m ?= n with
| Eq | Gt => m
| Lt => n
- end.
+ end.
-(** Characterization of maximum on binary integer numbers *)
+(** * Characterization of maximum on binary integer numbers *)
Lemma Zmax_case : forall (n m:Z) (P:Z -> Type), P n -> P m -> P (Zmax n m).
Proof.
-intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith.
+ intros n m P H1 H2; unfold Zmax in |- *; case (n ?= m); auto with arith.
Qed.
Lemma Zmax_case_strong : forall (n m:Z) (P:Z -> Type),
(m<=n -> P n) -> (n<=m -> P m) -> P (Zmax n m).
Proof.
-intros n m P H1 H2; unfold Zmax, Zle, Zge in *.
-rewrite <- (Zcompare_antisym n m) in H1.
-destruct (n ?= m); (apply H1|| apply H2); discriminate.
+ intros n m P H1 H2; unfold Zmax, Zle, Zge in *.
+ rewrite <- (Zcompare_antisym n m) in H1.
+ destruct (n ?= m); (apply H1|| apply H2); discriminate.
Qed.
-(** Least upper bound properties of max *)
+(** * Least upper bound properties of max *)
Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
Proof.
-intros; apply Zmax_case_strong; auto with zarith.
+ intros; apply Zmax_case_strong; auto with zarith.
Qed.
Notation Zmax1 := Zle_max_l (only parsing).
Lemma Zle_max_r : forall n m:Z, m <= Zmax n m.
Proof.
-intros; apply Zmax_case_strong; auto with zarith.
+ intros; apply Zmax_case_strong; auto with zarith.
Qed.
Notation Zmax2 := Zle_max_r (only parsing).
Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p.
Proof.
-intros; apply Zmax_case; assumption.
+ intros; apply Zmax_case; assumption.
Qed.
-(** Semi-lattice properties of max *)
+(** * Semi-lattice properties of max *)
Lemma Zmax_idempotent : forall n:Z, Zmax n n = n.
Proof.
-intros; apply Zmax_case; auto.
+ intros; apply Zmax_case; auto.
Qed.
Lemma Zmax_comm : forall n m:Z, Zmax n m = Zmax m n.
Proof.
-intros; do 2 apply Zmax_case_strong; intros;
- apply Zle_antisym; auto with zarith.
+ intros; do 2 apply Zmax_case_strong; intros;
+ apply Zle_antisym; auto with zarith.
Qed.
Lemma Zmax_assoc : forall n m p:Z, Zmax n (Zmax m p) = Zmax (Zmax n m) p.
Proof.
-intros n m p; repeat apply Zmax_case_strong; intros;
- reflexivity || (try apply Zle_antisym); eauto with zarith.
+ intros n m p; repeat apply Zmax_case_strong; intros;
+ reflexivity || (try apply Zle_antisym); eauto with zarith.
Qed.
-(** Additional properties of max *)
+(** * Additional properties of max *)
Lemma Zmax_irreducible_inf : forall n m:Z, Zmax n m = n \/ Zmax n m = m.
Proof.
-intros; apply Zmax_case; auto.
+ intros; apply Zmax_case; auto.
Qed.
Lemma Zmax_le_prime_inf : forall n m p:Z, p <= Zmax n m -> p <= n \/ p <= m.
Proof.
-intros n m p; apply Zmax_case; auto.
+ intros n m p; apply Zmax_case; auto.
Qed.
-(** Operations preserving max *)
+(** * Operations preserving max *)
Lemma Zsucc_max_distr :
forall n m:Z, Zsucc (Zmax n m) = Zmax (Zsucc n) (Zsucc m).
Proof.
-intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m);
- elim_compare n m; intros E; rewrite E; auto with arith.
+ intros n m; unfold Zmax in |- *; rewrite (Zcompare_succ_compat n m);
+ elim_compare n m; intros E; rewrite E; auto with arith.
Qed.
Lemma Zplus_max_distr_r : forall n m p:Z, Zmax (n + p) (m + p) = Zmax n m + p.
Proof.
-intros x y n; unfold Zmax in |- *.
-rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
- rewrite (Zcompare_plus_compat x y n).
-case (x ?= y); apply Zplus_comm.
+ intros x y n; unfold Zmax in |- *.
+ rewrite (Zplus_comm x n); rewrite (Zplus_comm y n);
+ rewrite (Zcompare_plus_compat x y n).
+ case (x ?= y); apply Zplus_comm.
Qed.