proposition: Lemma mindropeq_nil s : mindropeq [::] s = size s.
proof: Proof. rewrite /mindropeq; case: ex_minnP => m /= /eqP/esym dropm Hmin. apply anti_leq. have /esym/eqP/Hmin -> /= := drop_size s. by rewrite -drop_nilE dropm. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition