proposition: Lemma myandP: forall (b1 b2 : bool), reflect (b1 /\ b2) (b1 && b2).
proof: Proof. move=> b1 b2. case: b1. case b2. exact: ReflectT. apply: ReflectF. move=> h. by case: h. case b2. apply: ReflectF. move=> h. by case: h. apply: ReflectF. move=> h. by case: h. Qed.
imports: mathcomp(all_ssreflect)