proposition: Lemma lec_def x y : lec x y = (normC (y - x) == y - x).
proof: Proof. rewrite -subc_ge0; move: (_ - _) => [a b]; rewrite eq_complex /= eq_sym. have [<- /=|_] := altP eqP; last by rewrite andbF. by rewrite [0 ^+ _]mul0r addr0 andbT sqrtr_sqr ger0_def. 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)