proposition: Lemma alpha_plus_sup (alpha : Ord) (A : Ensemble Ord) : Inhabited A -> Countable A -> alpha + |_| A = |_| (image A (plus alpha)).
proof: Proof. intros H0 H1 ; generalize (@normal_plus_alpha alpha ). intros [H [H2 [H3 H4]]]; rewrite H4; auto. split. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)