proposition: Lemma mrank_subset s1 s2 : s1 \subset s2 -> mrank s1 <= mrank s2.
proof: Proof. move=> s1Ss2; apply/bigmax_leqP => e /andP[Hs1 Hs2]. by apply: leq_bigmax_cond; rewrite Hs1 (subset_trans Hs2). Qed.
imports: mathcomp(all_ssreflect)