proposition: Lemma Rseq_strictly_growing_trans : forall an, Rseq_strictly_growing an -> forall y x:nat, (x < y)%nat -> (an x < an y)%R.
proof: Proof. induction y. intros x Hx0. inversion Hx0. intros x Hxy. destruct (Compare.le_decide _ _ Hxy) as [Hyx|Hyx]. apply Rlt_trans with (an y). apply IHy. apply Nat.succ_le_mono. apply Hyx. apply H. rewrite <- Hyx. apply H. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra