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