proposition: Lemma diffv_eq0 U V : (U :\: V == 0)%VS = (U <= V)%VS.
proof: Proof. rewrite -dimv_eq0 -(eqn_add2l (\dim (U :&: V))) addn0 dimv_cap_compl eq_sym. by rewrite (dimv_leqif_eq (capvSl _ _)) (sameP capv_idPl eqP). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)