proposition: Lemma ler_norm2 (x : normedR2) : `|x| <= sqrt (Rsqr (fst x) + Rsqr (snd x)) <= Num.sqrt 2 * `|x|.
proof: Proof. rewrite RsqrtE; last by rewrite addr_ge0 //; apply/RleP/Rle_0_sqr. rewrite !Rsqr_pow2 !RpowE; apply/andP; split. by rewrite le_maxl; apply/andP; split; rewrite -[`|_|]sqrtr_sqr ler_wsqrtr // (lerDl, lerDr) sqr_ge0. wlog lex12 : x / (`|x.1| <= `|x.2|). move=> ler_norm; case: (lerP `|x.1| `|x.2|) => [/ler_norm|] //. rewrite lt_leAnge => /andP [lex21 _]. rewrite RplusE. by rewrite addrC [`|_|]maxC (ler_norm (x.2, x.1)). rewrite [`|_|]max_r // -[X in X * _]ger0_norm // -normrM. rewrite -sqrtr_sqr ler_wsqrtr // exprMn sqr_sqrtr // mulr_natl mulr2n lerD2r. rewrite -[_ ^+ 2]ger0_norm ?sqr_ge0 // -[X in _ <=X]ger0_norm ?sqr_ge0 //. by rewrite !normrX lerXn2r // nnegrE normr_ge0. Qed.
imports: Reals Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice fintype bigop order ssralg ssrnum) mathcomp(boolp reals Rstruct ereal) mathcomp(classical_sets signed topology normedtype landau)