proposition: Lemma Rseq_growing_trans : forall an, Rseq_growing an -> forall y x:nat, (x <= y)%nat -> (an x <= an y)%R.
proof: Proof. induction y. intros x Hxy; rewrite (proj1 (Nat.le_0_r x) Hxy); intuition (auto with real). intros x Hxy; destruct (Compare.le_decide _ _ Hxy) as [Hyx|Hyx]. apply Rle_trans with (an y). apply IHy. apply Nat.succ_le_mono. apply Hyx. apply H. subst; apply Rle_refl. Qed.
imports: Lia Reals Rsequence_def Rsequence_base_facts Rsequence_cv_facts Rsequence_rel_facts Rsequence_usual_facts Lra