diff --git a/classical/boolp.v b/classical/boolp.v index 3732baba09..50dafc1edb 100644 --- a/classical/boolp.v +++ b/classical/boolp.v @@ -635,21 +635,13 @@ by rewrite 2!negb_and -3!asbool_neg => /or3_asboolP. by rewrite 3!asbool_neg -2!negb_and => /and3_asboolP. Qed. -<<<<<<< HEAD Lemma notP (P : Prop) : ~ ~ P <-> P. Proof. by split => [|p]; [exact: contrapT|exact]. Qed. Lemma notE (P : Prop) : (~ ~ P) = P. Proof. by rewrite propeqE notP. Qed. -Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q. -Proof. by rewrite -(notP (_ /\ _)) not_andP 2!notE. Qed. -======= Lemma not_orE (P Q : Prop) : (~ (P \/ Q)) = ~ P /\ ~ Q. -Proof. -eqProp; [apply: contra_notP => /not_andP|apply: contraPnot => AB; apply/not_andP]; - by rewrite 2!notK. -Qed. ->>>>>>> f0e2f722 (contra tactic and helper lemmas (in boolp.v)) +Proof. by rewrite -[_ /\ _]notE not_andE 2!notE. Qed. Lemma not_orP (P Q : Prop) : ~ (P \/ Q) <-> ~ P /\ ~ Q. Proof. by rewrite not_orE. Qed. @@ -657,16 +649,8 @@ Proof. by rewrite not_orE. Qed. Lemma not_implyE (P Q : Prop) : (~ (P -> Q)) = (P /\ ~ Q). Proof. by rewrite propeqE not_implyP. Qed. -<<<<<<< HEAD -Lemma implyE (P Q : Prop) : (P -> Q) = (~ P \/ Q). -Proof. by rewrite -[LHS]notE not_implyE propeqE not_andP notE. Qed. - -Lemma orC (P Q : Prop) : (P \/ Q) = (Q \/ P). -Proof. by rewrite propeqE; split=> [[]|[]]; [right|left|right|left]. Qed. -======= Lemma orC : commutative or. Proof. by move=> P Q; rewrite propeqE; split; (case=> ?; [right|left]). Qed. ->>>>>>> f0e2f722 (contra tactic and helper lemmas (in boolp.v)) Lemma orA : associative or. Proof. by move=> P Q R; rewrite propeqE; split=> [|]; tauto. Qed. @@ -916,8 +900,6 @@ Proof. by apply/funeqP => ?; rewrite iterSr. Qed. Lemma iter0 {T} (f : T -> T) : iter 0 f = id. Proof. by []. Qed. -<<<<<<< HEAD -======= Section Inhabited. Variable (T : Type). @@ -929,4 +911,3 @@ Lemma inhabited_witness: inhabited T -> T. Proof. by rewrite inhabitedE => /cid[]. Qed. End Inhabited. ->>>>>>> f0e2f722 (contra tactic and helper lemmas (in boolp.v))