proposition: Lemma cond_eq : forall x y:R, (forall eps:R, 0 < eps -> Rabs (x - y) < eps) -> x = y.
proof: Proof. intros. destruct (total_order_T x y) as [[Hlt|Heq]|Hgt]. - cut (0 < y - x). + intro. assert (H1 := H (y - x) H0). rewrite <- Rabs_Ropp in H1. cut (- (x - y) = y - x); [ intro; rewrite H2 in H1 | ring ]. rewrite Rabs_right in H1. * elim (Rlt_irrefl _ H1). * left; assumption. + apply Rplus_lt_reg_l with x. rewrite Rplus_0_r; replace (x + (y - x)) with y; [ assumption | ring ]. - assumption. - cut (0 < x - y). + intro. assert (H1 := H (x - y) H0). rewrite Rabs_right in H1. * elim (Rlt_irrefl _ H1). * left; assumption. + apply Rplus_lt_reg_l with y. rewrite Rplus_0_r; replace (y + (x - y)) with x; [ assumption | ring ]. Qed.
imports: Rbase Rfunctions Rseries Lia