proposition: Lemma myiffP: forall (P Q : Prop) (b : bool), reflect P b -> (P -> Q) -> (Q -> P) -> reflect Q b.
proof: Proof. move=> P Q b Pb PQ QP. move: Pb. case: b. move=> h. case: h. move/PQ=> hp. by apply: ReflectT. move=> hNp. apply: ReflectF. move/QP=> hp. by move/hNp: hp. move=> h. case: h. move/PQ=> hq. by apply: ReflectT. move=> hNp. apply: ReflectF. move/QP=> hp. by move/hNp: hp. Qed.
imports: mathcomp(all_ssreflect)