proposition: Lemma ksi_plus_seq_n' : forall (m:nat), ksi + seq m <= beta.
proof: Proof. intro m ; destruct (Nat.le_gt_cases n m) as [H | H]. - apply ksi_plus_seq_n;auto. - apply le_trans with (ksi + seq n). + apply plus_mono_r_weak;auto. apply mono_seq_weak2; auto with arith. + apply ksi_plus_seq_n; auto with arith. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)