Mise en forme des theories

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 27 deletions

diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index a862c5619..6ea02a483 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -12,20 +12,20 @@ Require Import BinInt Zorder.
 
 Open Local Scope Z_scope.
 
-(** *** Lattice properties of min and max on Z *)
+(** Lattice properties of min and max on Z *)
 
 (** Absorption *)
 
 Lemma Zmin_max_absorption_r_r : forall n m, Zmax n (Zmin n m) = n.
 Proof.
-intros; apply Zmin_case_strong; intro; apply Zmax_case_strong; intro; 
-  reflexivity || apply Zle_antisym; trivial.
+  intros; apply Zmin_case_strong; intro; apply Zmax_case_strong; intro; 
+    reflexivity || apply Zle_antisym; trivial.
 Qed.
 
 Lemma Zmax_min_absorption_r_r : forall n m, Zmin n (Zmax n m) = n.
 Proof.
-intros; apply Zmax_case_strong; intro; apply Zmin_case_strong; intro; 
-  reflexivity || apply Zle_antisym; trivial.
+  intros; apply Zmax_case_strong; intro; apply Zmin_case_strong; intro; 
+    reflexivity || apply Zle_antisym; trivial.
 Qed.
 
 (** Distributivity *)
@@ -33,19 +33,19 @@ Qed.
 Lemma Zmax_min_distr_r : 
   forall n m p, Zmax n (Zmin m p) = Zmin (Zmax n m) (Zmax n p).
 Proof.
-intros.
-repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 
-  reflexivity ||
-  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+  intros.
+  repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 
+    reflexivity ||
+      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
 Qed.
 
 Lemma Zmin_max_distr_r : 
   forall n m p, Zmin n (Zmax m p) = Zmax (Zmin n m) (Zmin n p).
 Proof.
-intros.
-repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 
-  reflexivity ||
-  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+  intros.
+  repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 
+    reflexivity ||
+      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
 Qed.
 
 (** Modularity *)
@@ -53,30 +53,24 @@ Qed.
 Lemma Zmax_min_modular_r :
   forall n m p, Zmax n (Zmin m (Zmax n p)) = Zmin (Zmax n m) (Zmax n p).
 Proof.
-intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
-  reflexivity ||
-  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+  intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+    reflexivity ||
+      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
 Qed.
 
 Lemma Zmin_max_modular_r :
   forall n m p, Zmin n (Zmax m (Zmin n p)) = Zmax (Zmin n m) (Zmin n p).
 Proof.
-intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
-  reflexivity ||
-  apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
+  intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+    reflexivity ||
+      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).
 Qed.
 
 (** Disassociativity *)
 
 Lemma max_min_disassoc : forall n m p, Zmin n (Zmax m p) <= Zmax (Zmin n m) p.
 Proof.
-intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
-  apply Zle_refl || (assumption || eapply Zle_trans; eassumption).
+  intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;
+    apply Zle_refl || (assumption || eapply Zle_trans; eassumption).
 Qed.
 
-
-
-
-
-
-