proposition: Lemma mulsmxS m1 m2 m3 m4 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) (R3 : 'A_(m3, n)) (R4 : 'A_(m4, n)) : (R1 <= R3 -> R2 <= R4 -> R1 * R2 <= R3 * R4)%MS.
proof: Proof. move=> sR13 sR24; apply/mulsmx_subP=> A1 A2 R_A1 R_A2. by apply: mem_mulsmx; [apply: submx_trans sR13 | apply: submx_trans sR24]. 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)