proposition: Lemma formBd u v : u _|_ v -> '[u - v] = '[u] + '[v].
proof: Proof. by move=> uTv; rewrite formDd ?formN // normalE formNr oppr_eq0 -normalE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)