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