proposition: Lemma mindropeq_cons_eq a b s : a != b -> mindropeq (a :: s) (b :: s) = 1.
proof: Proof. rewrite /mindropeq; case: ex_minnP => m /= /eqP/esym dropm Hmin Hneq. apply anti_leq; rewrite {}Hmin //=. by case: m dropm => // /eqP; rewrite !drop0 eqseq_cons eq_sym (negbTE Hneq). Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition