proposition: Lemma ito_peirce : implies_to_or -> peirce.
proof: Proof. rewrite /peirce /peirce_law /implies_to_or=> H1 P Q H2. have X: P -> P by []. move: (H1 P P) =>/(_ X); case=>{X}// Pn. by apply: (H2)=>p. Qed.
imports: mathcomp(ssreflect)