proposition: Lemma XORequiv P Q: XOR P Q <-> XOR' P Q.
proof: Proof. split. - case; case=>[p|q] H. - by left; split=>// q; apply: H. by right; split=>// p; apply H. case; case=>p q. - split=>[| H]; first by left. by apply: q; case: H. split; first by right. by case=>/p. Qed.
imports: mathcomp(ssreflect ssrnat prime ssrbool eqtype)