proposition: Lemma normcM x y : normc (x * y) = normc x * normc y.
proof: Proof. move: x y => [a b] [c d] /=; rewrite -sqrtrM ?addr_ge0 ?sqr_ge0 //. rewrite sqrrB sqrrD mulrDl !mulrDr -!exprMn. rewrite mulrAC [b * d]mulrC !mulrA. suff -> : forall (u v w z t : R), (u - v + w) + (z + v + t) = u + w + (z + t). by rewrite addrAC !addrA. by move=> u v w z t; rewrite [_ - _ + _]addrAC [z + v]addrC !addrA addrNK. 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)