Minimisation utilisation NNPP

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

1 files changed, 15 insertions, 14 deletions

diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 1c1292fc8..ef4e89793 100755
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -17,24 +17,25 @@ Variable U : Type.
 
 (** de Morgan laws for quantifiers *)
 
-Lemma not_all_ex_not :
- forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.
+Lemma not_all_not_ex :
+ forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.
 Proof.
-unfold not in |- *; intros P notall.
-apply NNPP; unfold not in |- *.
+intros P notall.
+apply NNPP.
 intro abs.
-cut (forall n:U, P n); auto.
-intro n; apply NNPP.
-unfold not in |- *; intros.
-apply abs; exists n; trivial.
+apply notall.
+intros n H.
+apply abs; exists n; exact H.
 Qed.
 
-Lemma not_all_not_ex :
- forall P:U -> Prop, ~ (forall n:U, ~ P n) ->  exists n : U, P n.
+Lemma not_all_ex_not :
+ forall P:U -> Prop, ~ (forall n:U, P n) ->  exists n : U, ~ P n.
 Proof.
-intros P H.
-elim (not_all_ex_not (fun n:U => ~ P n) H); intros n Pn; exists n.
-apply NNPP; trivial.
+intros P notall.
+apply not_all_not_ex with (P:=fun x => ~ P x).
+intro all; apply notall.
+intro n; apply NNPP.
+apply all.
 Qed.
 
 Lemma not_ex_all_not :
@@ -67,4 +68,4 @@ unfold not in |- *; intros P allnot exP; elim exP; intros n p.
 apply allnot with n; auto.
 Qed.
 
-End Generic.
\ No newline at end of file
+End Generic.