proposition: Theorem shepherd_principle f c: function f -> (forall x, inc x (target f) -> cardinal (Vfi1 f x) = c) -> cardinal (source f) = (cardinal (target f)) *c c.
proof: Proof. move=> ff cc. set (pa := Lg (target f) (Vfi1 f)). have md: (mutually_disjoint pa). apply: mutually_disjoint_prop. rewrite/pa /Vfi1/Vfi; aw=> i j y it jt; rewrite !LgV// => sa sb. by rewrite (iim_fun_set1_hi ff sa) (iim_fun_set1_hi ff sb). have <-: unionb pa = source f. set_extens x. rewrite /pa; move /setUb_P; aw; move => [y ytf]; rewrite LgV//. move /iim_fun_P => [u /set1_P -> Jg];Wtac. move => xsf; move: (Vf_target ff xsf)=> Wt. apply /setUb_P; exists (Vf f x); rewrite /pa ? LgV //; aw; trivial. by apply: iim_fun_set1_i. transitivity (csum pa). apply :Eqc_disjointU; fprops. by rewrite /disjointU_fam; split;aww => i id; rewrite LgV //;aw. rewrite cprod2cl cprodC - csum_of_same (csum_pr pa) /pa; aw. by apply: csumb_exten; rewrite /pa; aw => t tf; rewrite LgV//; apply: cc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)