proposition: Lemma eq_close : forall x y : V, close x y -> x = y.
proof: Proof. intros x y H. apply plus_reg_r with (opp x). rewrite plus_opp_r. apply eq_sym, norm_eq_zero. apply Rle_antisym. 2: apply norm_ge_0. apply prop_eps. intros eps He. assert (He' : 0 < eps / norm_factor). apply Rdiv_lt_0_compat with (1 := He). apply norm_factor_gt_0. specialize (H (mkposreal _ He')). replace eps with (norm_factor * (eps / norm_factor)). apply norm_compat2 with (1 := H). field. apply Rgt_not_eq, norm_factor_gt_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub