proposition: Lemma mulid_addidr m n k (I : 'cV[R]_m) (J : 'cV[R]_n) (K : 'cV[R]_k) : (I *i (J +i K) <= (I *i J) +i (I *i K))%IS.
proof: Proof. apply/forallP=> /= i. apply: member_in. case/mxvec_indexP: i => i x. rewrite mxE mxvecE !mxE big_ord1 !mxE. case: splitP => j hj. exists (lshift (m*k)%nat (mxvec_index i j)). rewrite !mxE. case: splitP => ij /= hij. case/mxvec_indexP : ij hij => a b /= hab. have : enum_rank (i,j) = enum_rank (a,b) by apply/ord_inj. case/enum_rank_inj => -> ->. by rewrite mxE mxvecE !mxE big_ord_recl big_ord0 addr0 !mxE. case/mxvec_indexP : ij hij => a b /= hab. have : m * n <= enum_rank (i, j). by rewrite hab -{1}[(m * n)%nat]addn0 leq_add2l. rewrite leqNgt => /negP; case. by apply (leq_trans (ltn_ord _)); rewrite /= eq_card_prod // !card_ord. exists (rshift (m*n)%nat (mxvec_index i j)). rewrite !mxE. case: splitP => ij /= hij. case/mxvec_indexP : ij hij => a b /= hab. have : m * n <= enum_rank (a, b) by rewrite -hab -{1}[(m * n)%nat]addn0 leq_add2l. rewrite leqNgt => /negP; case. by apply (leq_trans (ltn_ord _)); rewrite /= eq_card_prod // !card_ord. case/mxvec_indexP : ij hij => a b /= hab. have : enum_rank (i,j) = enum_rank (a,b). apply/ord_inj/eqP. by rewrite -(eqn_add2l (m * n)%nat) hab. case/enum_rank_inj => -> ->. by rewrite mxE mxvecE !mxE big_ord_recl big_ord0 addr0 !mxE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice fingroup) mathcomp(matrix bigop zmodp mxalgebra poly) ssrcomplements