proposition: Theorem formDd u v : u _|_ v -> '[u + v] = '[u] + '[v].
proof: Proof. move=> uNv; rewrite formDl !formDr ['[v, u]]formC. by rewrite ['[u, v]](form_eq0P _) // rmorph0 mulr0 addr0 add0r. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix mxalgebra vector falgebra ssrnum algC algnum) mathcomp(fieldext) mathcomp(vector)