proposition: Remark supM_gt0 : zero < |_| M.
proof: Proof. destruct inhM as [x H]; apply lt_le_trans with x. - now destruct (OM H). - apply sup_upper_bound; auto with schutte. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)