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