proposition: Lemma norm_le_prod_norm_2 {K : AbsRing} {U V : NormedModule K} (x : U * V) : norm (snd x) <= norm x.
proof: Proof. eapply Rle_trans, sqrt_plus_sqr. rewrite (Rabs_pos_eq (norm (snd x))). apply Rmax_r. by apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv