proposition: Lemma normalE u v : (u _|_ v) = ('[u, v] == 0).
proof: Proof. by rewrite (sameP sub_kermxP eqP) mulmxA [_ *m _^t _]mx11_scalar fmorph_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)