proposition: Lemma inh_card_gt_O : forall X:Ensemble U, Inhabited U X -> forall n:nat, cardinal U X n -> n > 0.
proof: Proof. intros X [x HX] [] HCX. - now rewrite (cardinalO_empty X HCX) in HX. - apply Nat.lt_0_succ. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat