proposition: Lemma norm_triangle_inv : forall x y : V, Rabs (norm x - norm y) <= norm (minus x y).
proof: Proof. intros x y. apply Rabs_le_between' ; split. rewrite -(norm_opp (minus _ _)). apply Rle_minus_l ; eapply Rle_trans. 2 : apply norm_triangle. apply Req_le, f_equal. by rewrite /minus opp_plus plus_assoc plus_opp_r plus_zero_l opp_opp. eapply Rle_trans. 2 : apply norm_triangle. apply Req_le, f_equal. by rewrite /minus plus_comm -plus_assoc plus_opp_l plus_zero_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub