proposition: Lemma daddv_pi_add U V w : (U :&: V = 0)%VS -> (w \in U + V)%VS -> daddv_pi U V w + daddv_pi V U w = w.
proof: Proof. move/eqP; rewrite -dimv_eq0 memvE /subsetv /dimv !genmxE mxrank_eq0 => /eqP. by move=> dxUW UVw; rewrite unlock /= -linearD /= add_proj_mx ?v2rK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)