proposition: Lemma dmnan_ito : de_morgan_not_and_not -> implies_to_or.
proof: Proof. rewrite /de_morgan_not_and_not /implies_to_or=> H1 P Q Hi. suff: ~P \/ P. case=>//; first by left. - by move/ Hi; right. move: (H1 (~P) P)=> H2; apply: H2; case=> Hp p. suff: (P -> False) \/ False by case=>//. by apply: H1; case. Qed.
imports: mathcomp(ssreflect)