Essai où assert_style n'est utilisé que si pas visuellement une équation;

2 files changed, 10 insertions, 10 deletions

diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 2aac617eb..7d8ed5275 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -46,12 +46,12 @@ Proof.
   generalize (Z.ggcd_gcd a ('b)) (Zgcd_is_gcd a ('b))
     (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
   destruct (Z.ggcd a (Zpos b)) as (g,(aa,bb)).
-  simpl. intros <- Hg1 Hg2 (Hg3,Hg4).
-  assert (Hg0 : g <> 0) by (intro; now subst g).
+  simpl. intros <- Hg1 Hg2 (Hg3,Hg4). clear H0.
+  assert (Hg0 : g <> 0). (intro; now subst g). Show Proof.
   generalize (Z.ggcd_gcd c ('d)) (Zgcd_is_gcd c ('d))
     (Z.gcd_nonneg c ('d)) (Z.ggcd_correct_divisors c ('d)).
   destruct (Z.ggcd c (Zpos d)) as (g',(cc,dd)).
-  simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4).
+  simpl. intros <- Hg'1 Hg'2 (Hg'3,Hg'4). clear H0.
   assert (Hg'0 : g' <> 0) by (intro; now subst g').
 
   elim (rel_prime_cross_prod aa bb cc dd).
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 99b631905..be975e882 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -54,17 +54,17 @@ Theorem Z_lt_abs_rec :
 Proof.
   intros P HP p.
   set (Q := fun z => 0 <= z -> P z * P (- z)).
-  enough (H:Q (Z.abs p)) by
-    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
+  enough (H:Q (Z.abs p)) by admit.
+(*    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).*)
   apply (Z_lt_rec Q); auto with zarith.
   subst Q; intros x H.
   split; apply HP.
   - rewrite Z.abs_eq; auto; intros.
     destruct (H (Z.abs m)); auto with zarith.
-    destruct (Zabs_dec m) as [-> | ->]; trivial.
+    (* destruct (Zabs_dec m) as [-> | ->]; trivial. *) admit.
   - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
     destruct (H (Z.abs m)); auto with zarith.
-    destruct (Zabs_dec m) as [-> | ->]; trivial.
+    destruct (Zabs_dec m) as [-> | ->]; trivial; admit.
 Qed.
 
 Theorem Z_lt_abs_induction :
@@ -74,8 +74,8 @@ Theorem Z_lt_abs_induction :
 Proof.
   intros P HP p.
   set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.
-  enough (Q (Z.abs p)) by
-    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
+  enough (Q (Z.abs p)) by admit.
+(*    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).*)
   apply (Z_lt_induction Q); auto with zarith.
   subst Q; intros.
   split; apply HP.
@@ -84,7 +84,7 @@ Proof.
     elim (Zabs_dec m); intro eq; rewrite eq; trivial.
   - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
     destruct (H (Z.abs m)); auto with zarith.
-    destruct (Zabs_dec m) as [-> | ->]; trivial.
+    destruct (Zabs_dec m) as [-> | ->]; trivial; admit.
 Qed.
 
 (** To do case analysis over the sign of [z] *)