proposition: Lemma set_of_functions_sum2 E n: natp n -> cardinal(graphs_sum_le E (csucc n)) = (cardinal (graphs_sum_eq E (csucc n))) +c (cardinal (graphs_sum_le E n)).
proof: Proof. move => nN. have snN: natp (csucc n) by fprops. set A:= (graphs_sum_eq E (csucc n)). set B:= (graphs_sum_le E (csucc n)). set C:= (graphs_sum_le E n). have di: disjoint A C. apply: disjoint_pr. move=> u; move /(graphs_sum_eqP _ snN) => [_ pb _ _]. move /(graphs_sum_leP _ nN) => [_]. by rewrite pb => qa; move: (cleNgt qa (cltS nN)). suff: B = A \cup C by move => ->; rewrite (csum2_pr5 di) csum2cl csum2cr. set_extens t. move /(graphs_sum_leP _ snN) => [pa pb pc1 pc2]; apply /setU2_P. case: (equal_or_not (csum t) (csucc n)) => h. left; apply /(graphs_sum_eqP _ snN); split => //. right; apply /(graphs_sum_leP _ nN); split => //. by apply /(cltSleP nN); split. case /setU2_P. move /(graphs_sum_eqP _ snN) => [pa pb pc1 pc2]. apply /(graphs_sum_leP _ snN);split => //; rewrite pb; fprops. move /(graphs_sum_leP _ nN) => [pa pb pc1 pc2]. apply /(graphs_sum_leP _ snN);split => //. apply:cleT pb (cleS nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)