proposition: Lemma normalC p q (A : 'M_(p, n)) (B :'M_(q, n)) : (A _|_ B) = (B _|_ A).
proof: Proof. gen have nC : p q A B / A _|_ B -> B _|_ A; last by apply/idP/idP; apply/nC. move=> AnB; apply/normalP => u v ? ?; rewrite normalE. rewrite formC mulf_eq0 ?fmorph_eq0 ?signr_eq0 /=. by rewrite -normalE (normalP _ _ AnB). Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)