proposition: Lemma mono_seq_weak2 : forall i j, (i <= j)%nat -> seq i <= seq j.
proof: Proof. Proof with eauto with schutte. intros i j H; destruct (le_lt_eq_dec _ _ H). - right; now apply mono_seq2. - subst j; left ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)