Add contra tactics

Co-authored-by: Georges Gonthier <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -154,6 +154,20 @@
 - in `lebesgue_integral.v`:
   + `sigma_finite_measure` instance on product measure `\x`
 
+- file `contra.v`
+- in `contra.v`
+  + lemma `assume_not`
+  + tactic `assume_not`
+  + lemma `absurd_not`
+  + tactics `absurd_not`, `contrapose`
+  + tactic notations `contra`, `contra : constr(H)`, `contra : ident(H)`,
+    `contra : { hyp_list(Hs) } constr(H)`, `contra : { hyp_list(Hs) } ident(H)`,
+	 `contra : { - } constr(H)`
+  + lemma `absurd`
+  + tactic notations `absurd`, `absurd constr(P)`, `absurd : constr(H)`,
+    `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
+	 `absurd : { hyp_list(Hs) } ident(H)`
+
 - in `topology.v`:
   + lemma `filter_bigI_within`
   + lemma `near_powerset_map`

_CoqProject

@@ -10,6 +10,7 @@
 
 classical/all_classical.v
 classical/boolp.v
+classical/contra.v
 classical/classical_sets.v
 classical/mathcomp_extra.v
 classical/functions.v

classical/Make

@@ -8,6 +8,7 @@
 -arg -w -arg -projection-no-head-constant
 
 boolp.v
+contra.v
 classical_sets.v
 mathcomp_extra.v
 functions.v

classical/all_classical.v

@@ -1,4 +1,5 @@
 From mathcomp Require Export boolp.
+From mathcomp Require Export contra.
 From mathcomp Require Export classical_sets.
 From mathcomp Require Export mathcomp_extra.
 From mathcomp Require Export functions.