proposition: Lemma prj_fb f J: sub J (domain f) -> (forall i, inc i ((domain f) -s J) -> singletonp (Vg f i)) -> bijection_prop (pr_j f J) (productb f) (productb (Lg J (Vg f))).
proof: Proof. set (K:= ((domain f) -s J)) => sjd als. split; [| by rewrite/pr_j; aw | by rewrite/pr_j; aw]. have sk: sub K (domain f) by apply: sub_setC. have sr: singletonp (restriction_product f K). by apply:setX_set1;fprops; hnf; aw => i ik; rewrite LgV //; apply: als. set (g:= variantLc J K). have paa: prod_assoc_axioms f g by apply: (is_partition_with_complement sjd). set (f1:= prod_assoc_map f g). have bf1: bijection f1 by apply: pam_fb. have ff1:function f1 by fct_tac. set (xa:= restriction_product f (Vg g C0)). set (xb:= restriction_product f (Vg g C1)). set (f2:= inverse_fun (product2_canon xa xb)). have dg: domain g = C2 by rewrite /g; aw. have Va: Vg g C0 = J by rewrite /g; aw. have Vb: Vg g C1 = K by rewrite /g; aw. have bf2: bijection f2 by apply: inverse_bij_fb; apply: product2_canon_fb. have ff2: function f2 by fct_tac. have sf2tf1: source f2 = target f1. rewrite lf_target ifun_s lf_target dg; congr (productb _). by apply: Lg_exten=>//; move=> v vt; try_lvariant vt. set (f3:= first_proj (xa \times xb)). have sb: singletonp xb. by rewrite /xb /restriction_product Vb; apply: sr. have bf3: bijection f3 by apply: first_proj_fb. have sf3tf2: source f3 = target f2 by rewrite ifun_t ! lf_source. have cf3f3: f3 \coP f2 by rewrite /f3/f2; split=>//; fct_tac. have bcf3f2: bijection (f3 \co f2) by apply: compose_fb. have cf3f2f1: (f3 \co f2) \coP f1 by split; aw=>//; fct_tac. suff: (pr_j f J = (f3 \co f2) \co f1) by move=> ->; apply: compose_fb. have sp: source (pr_j f J) = source f1 by rewrite !lf_source. have nexb: nonempty xb by move/singletonP: sb => []. apply: function_exten; aw; trivial. by apply: prj_f=>//. by fct_tac. by rewrite !lf_target setX_domain // /xa Va. rewrite sp=> x xs. move xW: (Vf f1 x) =>y. move yW: (Vf f2 y)=>z. have yt: inc y (source f2) by rewrite -xW sf2tf1 ; fprops. have zt: inc z (target f2) by rewrite -yW; Wtac. have Jg2: (inc (kpair y z) (graph f2)) by rewrite -yW; Wtac. have fp: function (product2_canon xa xb) by apply: setX2_canon_f. have zs: inc z (source (product2_canon xa xb)) by move: zt; rewrite ifun_t. have zp: inc z (xa \times xb) by move: zs; rewrite lf_source. rewrite compfV // compfV //; last by rewrite xW. rewrite xW yW first_proj_V //. move: Jg2; rewrite /f2; aw; move/igraph_pP => Jg3. move: (Vf_pr2 fp Jg3); aw; rewrite setX2_canon_V =>//. move /(congr1 (Vg ^~C0)); aw => <-. move: xs; rewrite lf_source => xdd. have zd: inc C0 (domain g) by rewrite dg; fprops. by rewrite -xW /f1 pam_V // LgV // Va. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)