proposition: Lemma mindropeq_cons_neq a b s1 s2 : s1 != s2 -> mindropeq (a :: s1) (b :: s2) = (mindropeq s1 s2).+1.
proof: Proof. rewrite /mindropeq => Hneq; case: ex_minnP => m dropm Hminm. case: ex_minnP => n dropn Hminn; apply anti_leq. rewrite {}Hminm //=. case: m dropm => [|m {}/Hminn]/=; last by rewrite ltnS. by rewrite eqseq_cons (negbTE Hneq) andbF. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition