proposition: Lemma addv_pi1_pi2 U V w : w \in (U + V)%VS -> addv_pi1 U V w + addv_pi2 U V w = w.
proof: Proof. by rewrite -addv_diff; exact/daddv_pi_add/capv_diff. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)