proposition: Lemma nat_seq_growing_trans : forall an : nat -> nat, (forall x, an x <= an (S x)) -> forall y x, x <= y -> an x <= an y.
proof: Proof. induction y. intros x Hx0. rewrite <- (proj1 (Nat.le_0_r x) Hx0). apply Nat.le_refl. intros x Hxy. destruct (Compare.le_decide _ _ Hxy) as [Hyx|Hyx]. apply Nat.le_trans with (an y). apply IHy. apply Nat.succ_le_mono. apply Hyx. apply H. subst; apply Nat.le_refl. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra