proposition: Lemma mrank_mod s1 s2 : mrank (s1 :|: s2) + mrank (s1 :&: s2) <= mrank s1 + mrank s2.
proof: Proof. have [s3 [rS3 s3IM s3Ss1Is2]] := mrankE (s1 :&: s2). have s3Ss1Us2 : s3 \subset s1 :|: s2. apply: subset_trans s3Ss1Is2 _. by apply/subsetP => i; rewrite in_setI in_setU => /andP[->]. have [s4 s3Ss4 [<- s4IM s4Ss1Us2]] := mrank_compl s3IM s3Ss1Us2. pose s5 := s4 :&: s1; pose s6 := s4 :&: s2. have -> : s4 = s5 :|: s6 by rewrite -setIUr; apply/sym_equal/setIidPl. have /eqP-> : mrank (s1 :&: s2) == #|s5 :&: s6|. rewrite eqn_leq; apply/andP; split; last first. apply: leq_mrank. by apply: msets_sub s4IM; rewrite -setIA subsetIl. by apply: setISS; apply: subsetIr. rewrite -rS3; apply: subset_leq_card. by rewrite -setIIr subsetI s3Ss4. rewrite cardsUI. apply: leq_add. apply: leq_mrank => //; first by apply: msets_sub (subsetIl _ _) _. by apply: subsetIr. apply: leq_mrank => //; first by apply: msets_sub (subsetIl _ _) _. by apply: subsetIr. Qed.
imports: mathcomp(all_ssreflect)