proposition: Lemma sequence_cauchy : forall n p q, (p >= n)%nat -> (q >= n)%nat -> R_dist (Ln p) (Ln q) < (R_dist lb ub) * (/2) ^ n.
proof: Proof. intros n p q Hnp Hpq. assert (R_dist (Ln p) (Ln q) <= R_dist (fst (Dn n)) (snd (Dn n))). unfold R_dist; apply Rabs_include; apply sequence_bound; assumption. eapply Rle_lt_trans; [apply H|]. eapply Rle_lt_trans; [apply diagonal_dist|]. rewrite <- tech_pow_Rmult. replace (R_dist lb ub * (/2 * (/2) ^ n)) with ((R_dist lb ub * (/2) ^ n)/2) by field. apply epsilon_2; apply Rmult_lt_0_compat. apply non_zero_dist. apply pow_lt; lra. Qed.
imports: Reals Lra