proposition: Lemma xorP_gen (b1 b2 : bool)(P1 P2: Prop): reflect P1 b1 -> reflect P2 b2 -> reflect (XOR P1 P2) (xorb b1 b2).
proof: Proof. case=>H1; case=>H2; constructor; rewrite /XOR. - by case; case=>H; apply. - split; first by left. by case=>_ H; apply: H2. - split; first by right. by case=>H _; apply: H1. - intuition. Qed.
imports: mathcomp(ssreflect ssrnat prime ssrbool eqtype)