proposition: Lemma minset_exists P C : P C -> {A | minset P A & A \subset C}.
proof: Proof. move=> PC; have{PC}: exists A, P A && (A \subset C) by exists C; rewrite PC /=. case/ex_minset=> A /minsetP[/andP[PA sAC] minA]; exists A => //; apply/minsetP. by split=> // B PB sBA; rewrite (minA B) // PB (subset_trans sBA). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)