proposition: Lemma directv_addP {U V} : reflect (U :&: V = 0)%VS (directv (U + V)).
proof: Proof. by rewrite directv_addE !directv_trivial; apply: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)