proposition: Lemma set_of_functions_sum3 E: cardinal (graphs_sum_le E \0c) = \1c.
proof: Proof. have zb:= NS0. set w:= graphs_sum_le _ _. suff ->: (w = singleton (Lg E (fun _ =>\0c))) by apply: cardinal_set1. apply: set1_pr. apply /(graphs_sum_leP _ zb); aw;split; fprops. rewrite -/(csumb _ _) csum_of_same cprod0l; fprops. hnf; aw => t ti; rewrite LgV //; fprops. move => z /Zo_P [/gfunctions_P2 [pa pb pc] _]. rewrite - (Lg_recovers pa) - pb; apply: Lg_exten => i ie/=. by move: (pc _ (inc_V_range pa ie)); rewrite succ_zero => /set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)