proposition: Lemma dn_em : double_neg -> excluded_middle.
proof: Proof. rewrite /double_neg /excluded_middle=> Dn P. apply: (Dn (P \/ ~ P))=>H1; apply: (H1). by left; apply: (Dn)=> H2; apply: H1; right. Qed.
imports: mathcomp(ssreflect)