proposition: Lemma set_of_functions_sum1 E x n: natp n -> ~ (inc x E) -> (graphs_sum_le E n) \Eq (graphs_sum_eq (E +s1 x) n).
proof: Proof. move=> nN nxE. set (K:= Nintc n). set (f:= fun z=> z +s1 (J x (n -c (csum z)))). exists (Lf f (graphs_sum_le E n) (graphs_sum_eq (E +s1 x) n)). hnf;saw; apply: lf_bijective. + move => z /(graphs_sum_leP _ nN) [dz lez fgz alc]. apply /(graphs_sum_eqP _ nN). have p0: (fgraph (f z)) by apply: fgraph_setU1 => //; ue. have p1: (E +s1 x) = domain (f z) by rewrite -dz domain_setU1 //. have xd: inc x (domain (f z)) by rewrite -p1; fprops. have Vx2: Vg (f z) x = (n -c (csum z)) by rewrite /f setU1_V_out //; ue. have p2: cardinal_fam (f z). rewrite -dz in nxE; hnf. rewrite -p1; move=> i /setU1_P; case. rewrite -dz => idz; rewrite /f setU1_V_in //; apply: alc=>//. move => ->; rewrite Vx2; fprops. split => //. rewrite - (Lg_recovers p0) -p1 -/(csumb _ _) csumA_setU1 // -dz /csumb. have ->: (Lg (domain z) (Vg (f z))) = z. apply /fgraph_exten => //;aw; fprops => t tf; rewrite /f LgV //. rewrite setU1_V_in => //; ue. by rewrite Vx2; apply:cdiff_pr. + move => u v /(graphs_sum_leP _ nN) [fu su tu _]. move /(graphs_sum_leP _ nN) => [fv sv tv _]. apply: extension_injective => //; ue. + move=> y /(graphs_sum_eqP _ nN) [fy sy ty suy]. have pa: fgraph (Lg E (Vg y)) by fprops. have pb: cardinal_fam (Lg E (Vg y)). hnf; aw => t tE; rewrite LgV//; apply: suy; rewrite fy; fprops. have pc : n = csum (Lg E (Vg y)) +c Vg y x. rewrite - sy -{1} (Lg_recovers ty) -/(csumb (domain y) _). by rewrite fy (csumA_setU1 _ nxE). have pd: Vg y x = n -c csum (Lg E (Vg y)). rewrite pc in nN; rewrite pc csumC cdiff_pr1 //. apply: (NS_in_sumr _ nN); apply: suy; rewrite fy; fprops. apply: (NS_in_suml _ nN); fprops. exists (Lg E (Vg y)). apply /(graphs_sum_leP _ nN); saw; rewrite pc. apply:csum_M0le; fprops. symmetry; rewrite /f;apply: fgraph_exten; fprops. + by apply fgraph_setU1; fprops; aw. + by rewrite domain_setU1; aw. + rewrite domain_setU1; aw => t; case /setU1_P => te. by rewrite setU1_V_in // ? LgV//; aw. by rewrite te setU1_V_out //; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)