proposition: Lemma sequence_cauchy_crit : Cauchy_crit Ln.
proof: Proof. intros eps H. assert (Hinf: (Rabs (/ 2)) < 1). rewrite Rabs_right; lra. destruct (pow_lt_1_zero (/2) Hinf (eps / (R_dist lb ub))) as [n M]. apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply non_zero_dist. exists n. intros p q Hp Hq. eapply Rlt_trans. apply sequence_cauchy; [apply Hp|apply Hq]. let t := type of (M n (Nat.le_refl n)) in assert (Hr: t). apply M; apply Nat.le_refl. rewrite Rabs_right in Hr. unfold Rdiv in Hr. apply Rmult_lt_reg_l with (r := / R_dist lb ub). apply Rinv_0_lt_compat; apply non_zero_dist. rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_l; rewrite Rmult_comm; exact Hr. apply Rgt_not_eq; apply non_zero_dist. apply Rle_ge; apply pow_le; lra. Qed.
imports: Reals Lra