proposition: Lemma cprod_inf_eq x y i: fgraph x -> fgraph y -> (domain x = domain y) -> inc i (domain x) -> (Vg x i) <> \0c -> Vg y i <> \0c -> (exists j, [/\ inc j (domain x), j <> i, infinite_c (Vg x j), Vg x i <=c Vg x j & Vg y i <=c Vg x j]) -> (forall j, inc j (domain x) -> j = i \/ Vg x j = Vg y j) -> cprod x = cprod y.
proof: Proof. move => pa pb pc pd pe pf [j [qa qb qc qd qe]] ph. set x' := Lg (domain x) (fun z => Yo (z = i) (Vg x j) (Vg x z)). set y' := Lg (domain y) (fun z => Yo (z = i) (Vg y j) (Vg y z)). have svj: Vg x j = Vg y j by case: (ph _ qa) => // aux; by case: qb. have sp: x' = y'. rewrite /x' /y' -pc; apply: Lg_exten => k kdx; aw; Ytac xeq; Ytac0 => //. case: (ph _ kdx) => // aux. suff: forall z, fgraph z -> inc i (domain z) -> Vg z i <> \0c -> inc j (domain z) -> j <> i -> infinite_c (Vg z j) -> Vg z i <=c Vg z j -> cprod z = cprod (Lg (domain z)(fun t => Yo (t = i)(Vg z j) (Vg z t))). move => aux. rewrite (aux x pa pd pe qa qb qc qd) -/ x'. rewrite pc in pd qa; rewrite svj in qc qe. by rewrite (aux y pb pd pf qa qb qc qe) -/ y' sp. move => z fgz idz jdz znz jni iv jv. set z1 := (Lg (domain z) (fun t => Yo (t = i) (Vg z j) (Vg z t))). move: (setC1_K idz); set j1 := (domain z) -s1 i => pA. symmetry in pA. have aux1: ~ inc i j1 by move /setC_P => [_] /set1_P; case. rewrite (induction_prod1 pA aux1). have fgz1: fgraph z1 by rewrite /z1; fprops. have pN: domain z1 = j1 +s1 i by rewrite /z1; aw. rewrite (induction_prod1 pN aux1). have fg2: fgraph (restr z j1) by fprops. have fg3: fgraph (restr z1 j1) by fprops. have pC: sub j1 (domain z) by move => t /setC1_P []. have pD: sub j1 (domain z1) by rewrite /z1; aw. have jj: inc j j1 by apply /setC1_P; split => //. have dr1: (domain (restr z j1)) = j1 by aw. have dr2: (domain (restr z1 j1)) = j1 by aw. have jdz1: inc j (domain (restr z j1)) by ue. move: (setC1_K jdz1); set j2 := _ -s1 j => pE. symmetry in pE. have aux2: ~ inc j j2 by move /setC1_P=> [_]. rewrite (induction_prod1 pE aux2). rewrite dr1 -dr2 in pE. rewrite (induction_prod1 pE aux2) - cprodA - cprodA. have sc: sub j2 j1 by move => t /setC1_P []; rewrite dr1. move: (sub_trans sc pC) => sd. rewrite (double_restr _ sc) (double_restr _ sc). rewrite /z1 !LgV//; Ytac0; Ytac0; apply:f_equal2. apply:f_equal; apply: fgraph_exten; aww. move=> k kj2. have k2: inc k (domain z) by apply: sd. by rewrite !LgV//;Ytac ki; [ move: (sc _ kj2); rewrite ki |]. by rewrite (cprod_inf jv iv jdz) (csquare_inf iv). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)