proposition: Lemma lec_normD x y : lec (normC (x + y)) (normC x + normC y).
proof: Proof. move: x y => [a b] [c d] /=; simpc; rewrite addr0 eqxx /=. rewrite -(@ler_pexpn2r _ 2) -?topredE /= ?(ler_paddr, sqrtr_ge0) //. rewrite [X in _ <= X] sqrrD ?sqr_sqrtr; do ?by rewrite ?(ler_paddr, sqrtr_ge0, sqr_ge0, mulr_ge0) //. rewrite -addrA addrCA (monoRL (addrNK _) (ler_add2r _)) !sqrrD. set u := _ *+ 2; set v := _ *+ 2. rewrite [a ^+ _ + _ + _]addrAC [b ^+ _ + _ + _]addrAC -addrA. rewrite [u + _] addrC [X in _ - X]addrAC [b ^+ _ + _]addrC. rewrite [u]lock [v]lock !addrA; set x := (a ^+ 2 + _ + _ + _). rewrite -addrA addrC addKr -!lock addrC. have [huv|] := ger0P (u + v); last first. by move=> /ltW /le_trans -> //; rewrite pmulrn_lge0 // mulr_ge0 ?sqrtr_ge0. rewrite -(@ler_pexpn2r _ 2) -?topredE //=; last first. by rewrite ?(pmulrn_lge0, mulr_ge0, sqrtr_ge0) //. rewrite -mulr_natl !exprMn !sqr_sqrtr ?(ler_paddr, sqr_ge0) //. rewrite -mulrnDl -mulr_natl !exprMn ler_pmul2l ?exprn_gt0 ?ltr0n //. rewrite sqrrD mulrDl !mulrDr -!exprMn addrAC -!addrA ler_add2l !addrA. rewrite [_ + (b * d) ^+ 2]addrC -addrA ler_add2l. have: 0 <= (a * d - b * c) ^+ 2 by rewrite sqr_ge0. by rewrite sqrrB addrAC subr_ge0 [_ * c]mulrC mulrACA [d * _]mulrC. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrint div ssrnum rat poly closed_field) mathcomp(polyrcf matrix mxalgebra tuple mxpoly zmodp binomial realalg) mathcomp(mxpoly)