proposition: Lemma norm_gt_0 : forall x : V, x <> zero -> 0 < norm x.
proof: Proof. intros x Hx. apply Rnot_le_lt. contradict Hx. apply norm_eq_zero. apply Rle_antisym with (1 := Hx). apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub