proposition: Lemma below_smallest P U V : smallest P U -> #|V| < #|U| -> ~ P V.
proof: Proof. move => [_ small_U]; rewrite ltnNge; exact/contraNnot/small_U. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)