proposition: Remark ksi_plus_seq_n : forall (m:nat), (n <= m)%nat -> ksi + seq m <= beta.
proof: Proof. Proof with eauto with schutte. intros m H; apply le_trans with (seq (S m)). - simpl; apply plus_mono_weak_l. + apply le_trans with (seq n). * right; unfold n, some; pattern (epsilon InHWit (fun n0 : nat => ksi < seq n0)); apply epsilon_ind. apply lt_beta_exists. elim H; auto. * destruct (le_lt_eq_dec n m H). right; apply mono_seq2; auto. subst m;left; split ... - right;apply lt_omega_limit. + apply seq_mono_intro ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)