proposition: Remark mono_seq : forall i, seq i < seq (S i).
proof: Proof. Proof with eauto with schutte. induction i. - simpl; pattern (succ alpha) at 1. rewrite <- alpha_plus_zero; apply plus_mono_r ... - simpl in *. pattern (seq i + seq i) at 1; rewrite <- alpha_plus_zero; apply plus_mono_r ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)