proposition: Lemma daddv_pi_proj U V w (pi := daddv_pi U V) : (U :&: V = 0)%VS -> pi (pi w) = pi w.
proof: Proof. by move/daddv_pi_id=> -> //; apply: memv_pi. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)