proposition: Lemma dimv_sum_leqif (S : addv_expr) : \dim (unwrap S) <= unwrap (addv_dim S) ?= iff directv (unwrap S).
proof: Proof. rewrite directvE; case: S => [[U] [d] /= defUd]; split=> //=. rewrite /dimv; elim: {1}_ {U}_ d / defUd => // m1 m2 A1 A2 r1 r2 _ leA1 _ leA2. by apply: leq_trans (leq_add leA1 leA2); rewrite mxrank_adds_leqif. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)