proposition: Lemma norm_ge_0 : forall x : V, 0 <= norm x.
proof: Proof. intros x. apply Rmult_le_reg_l with 2. by apply Rlt_0_2. rewrite Rmult_0_r -norm_zero -(plus_opp_r x). apply Rle_trans with (norm x + norm (opp x)). apply norm_triangle. apply Req_le ; rewrite norm_opp. ring. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub