proposition: Lemma norm_prod {K : AbsRing} {U : NormedModule K} {V : NormedModule K} (x : U) (y : V) : Rmax (norm x) (norm y) <= norm (x,y) <= sqrt 2 * Rmax (norm x) (norm y).
proof: Proof. rewrite -(Rabs_pos_eq (norm x)). rewrite -(Rabs_pos_eq (norm y)). apply sqrt_plus_sqr. by apply norm_ge_0. by apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub