proposition: Lemma em_dmnan: excluded_middle -> de_morgan_not_and_not.
proof: Proof. rewrite /excluded_middle /de_morgan_not_and_not=> H1 P Q H2. suff: ~P -> Q. - move=>H3. move: (H1 P); case=>//X; first by left. by right; apply: H3. move=> Pn. move: (H1 Q); case=>// Qn. suff: False=>//; apply: H2; split=>//. Qed.
imports: mathcomp(ssreflect)