proposition: Lemma mindropeq_eq s : mindropeq s s = 0.
proof: Proof. rewrite /mindropeq; case: ex_minnP => m _ /(_ 0 (eqxx _)). by rewrite leqn0 => /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools sorted partition