proposition: Lemma nat_seq_strict_growing_trans : forall an, (forall x, an x < an (S x)) -> forall y x, x < y -> an x < an y.
proof: Proof. induction y. intros x Hx0. inversion Hx0. 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 Nat.lt_le_incl. apply H. rewrite <- Hyx. apply H. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra