proposition: Lemma graphs_sum_eqP F n: natp n -> forall f, inc f (graphs_sum_eq F n) <-> [/\ domain f = F, csum f = n, fgraph f & cardinal_fam f].
proof: Proof. move=> nN f. split. move=> /Zo_P [/gfunctions_P2 [qa qb qc] qd]; split => //. by move => i idf; case /(NleP nN): (qc _ (inc_V_range qa idf)). move =>[qa qb qc qd]; apply: Zo_i => //; apply/gfunctions_P2; split => //. move => t /(range_gP qc) [i idf ->]; apply /(NleP nN). rewrite - qb; exact: (csum_increasing6 (qd i idf) idf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)