proposition: Lemma set_of_functions_sum4 n: natp n -> cardinal (graphs_sum_le emptyset n) = \1c.
proof: Proof. move=> nN. suff: (graphs_sum_le emptyset n =singleton emptyset). by move=> ->;apply: cardinal_set1. apply: set1_pr. apply /(graphs_sum_leP _ nN);split; [by aw | | fprops | ]. + rewrite csum_trivial; aww; exact (cle0n nN). + apply: fgraph_set0. + by move => t;rewrite domain_set0 => /in_set0. by move => z/ (graphs_sum_leP _ nN) [ /domain_set0_P g df _ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)