proposition: Lemma Req_lt_aux : forall x y, (forall eps : posreal, Rabs (x - y) < eps) -> x = y.
proof: Proof. intros. apply Rminus_diag_uniq. apply Rabs_eq_0. apply Rle_antisym. apply le_epsilon. intros. rewrite Rplus_0_l. apply Rlt_le. apply (H (mkposreal eps H0)). apply Rabs_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)