proposition: Lemma mindropeq_leq s1 s2 : mindropeq s1 s2 <= maxn (size s1) (size s2).
proof: Proof. rewrite /mindropeq; case: ex_minnP => m _; apply. by rewrite !drop_oversize ?leq_maxr ?leq_maxl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition