proposition: Lemma ex4_compose_f i j k (psf := ex4_function_f_fam): gle r i j -> gle r j k -> Vg psf (J i j) \co Vg psf (J j k) = Vg psf (J i k).
proof: Proof. move => lij ljk. move:(ex4H) => [_ or sr _ _]. have lik: gle r i k by order_tac. rewrite /psf /ex4_function_f_fam LgV//. move:(ex4_function_f_fun lij) => [fij sij tij]. move:(ex4_function_f_fun lik) => [fik sik tik]. move:(ex4_function_f_fun ljk) => [fjk sjk tjk]. move:(ex4_function_f_ax lij) => axij. move:(ex4_function_f_ax lik) => axik. move:(ex4_function_f_ax ljk) => axjk. have co: ex4_function_f (J i j) \coP ex4_function_f (J j k). split; fprops; ue. rewrite !LgV //;apply:function_exten;aw; trivial; try ue; first by fct_tac; ue. rewrite sjk => x xv; rewrite compfV//; try ue. rewrite /ex4_function_f; aw. rewrite (LfV axik xv) (LfV axjk xv) (LfV axij (axjk _ xv)). clear fij sij tij fik sik tjk fjk sjk tik axij axik axjk co. move/Zo_P: xv => [xF rx]; rewrite - rx in ljk lik. move:(ex4_function_f_prop1 xF ljk) => [y3F y3r]. have lij': gle r i (ex4_fct_r (ex4_function_fv j x)) by rewrite y3r. set y3 := (ex4_function_fv j x). rewrite /ex4_function_fv. set i1 := (ex4_indexj x i). set i2 := (ex4_indexj x j). set y1 := (restr x (csucc i1)). set y2 := (restr x (csucc i2)). move: (ex4_indexj_correct y3F lij'). move: (ex4_indexj_correct xF ljk). move: (ex4_indexj_correct xF lik). rewrite -/i1 -/i2; move =>[i1p1 i1p2 i1p3] [i2p1 i2p2 i2p3]. rewrite -/y3; set i3 := ex4_indexj y3 i;move => [i3p1 i3p2 i3p3]. move:(or) => [_ _ ot _]. have li1i2: i1 <=c i2 by apply: (i1p3 _ i2p1); apply:(ot _ _ _ lij i2p2). have dy3: domain y3 = csucc i2. by rewrite /y3 /ex4_function_fv /ex4_modify_r; aw. rewrite dy3 in i3p1 i3p3. have nN: (natp (domain x)) by move/ex4_inF_hi:xF => [_ []]. have i1N := NS_lt_nat i1p1 nN. have i2N := NS_lt_nat i2p1 nN. have lei3i2: i3 <=c i2 by apply/(cltSleP i2N). have i3N := NS_le_nat lei3i2 i2N. have lt0: i1 <c csucc i2 by apply/(cltSleP i2N). have lt1: inc i1 (csucc i2) by apply /(NltP (NS_succ i2N)). have lei3i1: i3 <=c i1. apply: (i3p3 _ lt0). rewrite /y3 /ex4_function_fv /ex4_modify_r -/i2/ex4_last; aw. rewrite (LgV lt1) LgV// (cpred_pr2 i2N). Ytac eq1; aw; trivial. have lt2: inc i3 (csucc i2) by apply /(NltP (NS_succ i2N)). have lei1i3: i1 <=c i3. case: (equal_or_not i3 i2) => eqa; first by rewrite eqa. apply: (i1p3 _ (cle_ltT lei3i2 i2p1)). move: i3p2; rewrite /y3 /ex4_function_fv /ex4_modify_r -/i2/ex4_last. by aw;rewrite ! LgV// (cpred_pr2 i2N); Ytac0. have ei1i3: i1 = i3 by apply:cleA. have dy1: domain y1 = csucc i1 by rewrite /y1 restr_d. rewrite /ex4_modify_r; apply: fgraph_exten; try apply: Lg_fgraph. by rewrite 2!Lgd dy1 restr_d ei1i3. rewrite Lgd restr_d dy1 - ei1i3 => t ts3; rewrite LgV//. have lt3: t <=c i1 by apply/(cltSleP i1N); apply/(NltP (NS_succ i1N)). have lt4: inc t (csucc i2). apply/(NltP (NS_succ i2N)); apply/(cltSleP i2N); apply: (cleT lt3 li1i2). rewrite /ex4_last restr_d dy1 (cpred_pr2 i1N); rewrite LgV // LgV//. rewrite /y3 /ex4_function_fv /ex4_modify_r restr_d - /i2 (LgV lt4). rewrite (restr_ev _ lt4) /ex4_last restr_d (cpred_pr2 i2N) /y1 (restr_ev _ ts3). Ytac eqa; Ytac0; Ytac eqc => //; aw; trivial. by case:(cleNgt (li1i2)); rewrite - eqc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)