proposition: Lemma sub_fgraphsP A B f: inc f (sub_fgraphs A B) <-> exists2 C, sub C A & inc f (gfunctions C B).
proof: Proof. split. by move/setUf_P => [z /setP_P zx h ] ; exists z. move => [C /setP_P ca cb]; apply /setUf_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)