proposition: Lemma norm_opp : forall x : V, norm (opp x) = norm x.
proof: Proof. intros x. apply Rle_antisym. - rewrite -scal_opp_one. rewrite -(Rmult_1_l (norm x)) -(@abs_opp_one K). apply norm_scal. - rewrite -{1}[x]opp_opp -scal_opp_one. rewrite -(Rmult_1_l (norm (opp x))) -(@abs_opp_one K). apply norm_scal. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub