proposition: Lemma norm_minus_gt_0 : forall x y : V, x <> y -> 0 < norm (minus x y).
proof: Proof. intros x y Hxy. apply norm_gt_0. contradict Hxy. apply plus_reg_r with (opp y). now rewrite plus_opp_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub