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, 13 insertions, 10 deletions

diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 6578f6c85..938d514df 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -13,16 +13,19 @@ Require Export Relation_Operators.
 Require Export Operators_Properties.
 
 Lemma inverse_image_of_equivalence :
- forall (A B:Set) (f:A -> B) (r:relation B),
-   equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
-intros; split; elim H; red in |- *; auto.
-intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
+  forall (A B:Set) (f:A -> B) (r:relation B),
+    equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
+Proof.
+  intros; split; elim H; red in |- *; auto.
+  intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
 Lemma inverse_image_of_eq :
- forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
-split; red in |- *;
- [  (* reflexivity *) reflexivity
- |  (* transitivity *) intros; transitivity (f y); assumption
- |  (* symmetry *) intros; symmetry  in |- *; assumption ].
-Qed.
\ No newline at end of file
+  forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+Proof.
+  split; red in |- *;
+    [  (* reflexivity *) reflexivity
+      |  (* transitivity *) intros; transitivity (f y); assumption
+      |  (* symmetry *) intros; symmetry  in |- *; assumption ].
+Qed.
+