proposition: Lemma AP_mult_Sn_closed (alpha beta: Ord) : AP alpha -> beta < alpha -> forall n, mult_Sn beta n < alpha.
proof: Proof. intros H H0; induction n. - now simpl. - simpl. now apply AP_plus_closed. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)