proposition: Lemma ex_smallest A : P A -> exists B, smallest P B.
proof: Proof. move=> /PP PA. exists [arg min_(B < A | p B) #|B|]. exact/smallestPP/argmin_smallest. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)