proposition: Lemma mono_seq2 : forall i j, (i < j)%nat -> seq i < seq j.
proof: Proof. Proof with auto. induction 1. - apply mono_seq ... - apply lt_trans with (seq m). apply IHle. apply mono_seq ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)