proposition: Lemma directv_addE (S1 S2 : addv_expr) : directv (unwrap S1 + unwrap S2) = [&& directv (unwrap S1), directv (unwrap S2) & unwrap S1 :&: unwrap S2 == 0]%VS.
proof: Proof. by rewrite /directv_def /dimv vs2mxD -mxdirectE mxdirect_addsE -vs2mxI -vs2mx0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)