proposition: Lemma mindropeq0 s1 s2 : mindropeq s1 s2 = 0 -> s1 = s2.
proof: Proof. rewrite /mindropeq; case: ex_minnP => m /eqP eqdrop _ meq0. by move: eqdrop; rewrite meq0 !drop0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition