proposition: Lemma AP_mult_fin_r_closed (alpha beta: Ord) : AP alpha -> beta < alpha -> forall n, beta * n < alpha.
proof: Proof. destruct n. - simpl; eapply le_lt_trans ; eauto with schutte. - simpl; now apply AP_mult_Sn_closed. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)