fix failed rebase

classical/boolp.v

@@ -635,38 +635,25 @@ 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.
 
 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 +903,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 +914,3 @@ Lemma inhabited_witness: inhabited T -> T.
 Proof. by rewrite inhabitedE => /cid[]. Qed.
 
 End Inhabited.
->>>>>>> f0e2f722 (contra tactic and helper lemmas (in boolp.v))