proposition: Lemma mxrank_sum_leqif m n (S : mxsum_expr m n) : \rank (unwrap S) <= unwrap (mxsum_rank S) ?= iff mxdirect (unwrap S).
proof: Proof. rewrite /mxdirect_def; case: S => [[A] [r] /= defAr]; split=> //=. elim: m A r / defAr => // m1 m2 A1 A2 r1 r2 _ leAr1 _ leAr2. by apply: leq_trans (leq_add leAr1 leAr2); rewrite mxrank_adds_leqif. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)