Merge pull request #499 from chdoc/contra-prop

contra lemmas involving propositions

1 files changed, 13 insertions, 1 deletions

diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index bd58e01..1391b5b 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -208,7 +208,7 @@ Arguments eqVneq {T} x y, {T x y}.
 Section Contrapositives.
 
 Variables (T1 T2 : eqType).
-Implicit Types (A : pred T1) (b : bool) (x : T1) (z : T2).
+Implicit Types (A : pred T1) (b : bool) (P : Prop) (x : T1) (z : T2).
 
 Lemma contraTeq b x y : (x != y -> ~~ b) -> b -> x = y.
 Proof. by move=> imp hyp; apply/eqP; apply: contraTT hyp. Qed.
@@ -219,6 +219,12 @@ Proof. by move=> imp hyp; apply/eqP; apply: contraNT hyp. Qed.
 Lemma contraFeq b x y : (x != y -> b) -> b = false -> x = y.
 Proof. by move=> imp /negbT; apply: contraNeq. Qed.
 
+Lemma contraPeq P x y : (x != y -> ~ P) -> P -> x = y.
+Proof. by move => imp HP; apply: contraTeq isT => /imp /(_ HP). Qed.
+
+Lemma contra_not_eq P x y : (x != y -> P) -> ~ P -> x = y.
+Proof. by move => imp; apply: contraPeq => /imp HP /(_ HP). Qed.
+
 Lemma contraTneq b x y : (x = y -> ~~ b) -> b -> x != y.
 Proof. by move=> imp; apply: contraTN => /eqP. Qed.
 
@@ -228,6 +234,9 @@ Proof. by move=> imp; apply: contraNN => /eqP. Qed.
 Lemma contraFneq b x y : (x = y -> b) -> b = false -> x != y.
 Proof. by move=> imp /negbT; apply: contraNneq. Qed.
 
+Lemma contraPneq P x y : (x = y -> ~ P) -> P -> x != y.
+Proof. by move => imp; apply: contraPN => /eqP. Qed.
+
 Lemma contra_eqN b x y : (b -> x != y) -> x = y -> ~~ b.
 Proof. by move=> imp /eqP; apply: contraL. Qed.
 
@@ -246,6 +255,9 @@ Proof. by move=> imp; apply: contraNF => /imp->. Qed.
 Lemma contra_neqT b x y : (~~ b -> x = y) -> x != y -> b.
 Proof. by move=> imp; apply: contraNT => /imp->. Qed.
 
+Lemma contra_neq_not P x y : (P -> x = y) -> x != y -> ~ P.
+Proof. by move => imp;apply: contraNnot => /imp->. Qed.
+
 Lemma contra_eq z1 z2 x1 x2 : (x1 != x2 -> z1 != z2) -> z1 = z2 -> x1 = x2.
 Proof. by move=> imp /eqP; apply: contraTeq. Qed.