proposition: Lemma increase_seq_transit (u : nat -> R) : (forall n : nat, Rlt (u n) (u (S n))) -> (forall n m : nat, n < m -> Rlt (u n) (u m)).
proof: Proof. intros. induction m. - intros. inversion H0. - intros. destruct (split_lt_succ n m H0). + apply (Rlt_trans (u n) (u m)). * apply IHm. assumption. * apply H. + subst. apply H. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon