proposition: Lemma nat_seq_growing_trans_converse : forall an, (forall x, an x < an (S x)) -> forall x y, an x <= an y -> x <= y.
proof: Proof. intros an H x y Hxy. destruct (le_le_S_dec x y). assumption. pose proof (nat_seq_strict_growing_trans an H x y). intuition lia. Qed.
imports: Reals Rsequence_def Rsequence_facts Lia Lra