proposition: Lemma ex6_res4 i j k: gle rL i j -> gle rL j k -> ex6_gij (J j k) \co ex6_gij (J i j) = ex6_gij (J i k).
proof: Proof. move => lij ljk; move: (proj33 HLp _ _ _ lij ljk) => lik. move:(ex6_res2 lij) => [fij sij tij]. move:(ex6_res2 lik) => [fik sik tik]. move:(ex6_res2 ljk) => [fjk sjk tjk]. have cop: ex6_gij (J j k) \coP ex6_gij (J i j) by split => //; ue. apply:function_exten. - by apply:compf_f. - exact. - by aw; ue. - by aw; ue. - aw; rewrite sij => x xs. move: (arg1_sr lij)(arg2_sr lij) (arg2_sr ljk); rewrite HLs => iL jL kL. have xs': inc x (source (ex6_gij (J i j))) by ue. rewrite (compfV cop xs') !ex6_gij_prop1; clear cop xs'. move: xs; rewrite (ex6_res1 lij) => /inductive_limit_hi /= [Qx Px1 xv]. have s1:sub (Vg Jf i) (Vg Jf j) by apply:HJm. have Px2:inc (P (rep x)) (Vg (isE (ex6_systemi j)) (Q (rep x))). move: Px1; simpl; rewrite LgV//. have Px3: inc (P (rep x)) (Vg (isE S) (Q (rep x))). by move: Px1; rewrite (proj41 (ex6_prop5b jL)) double_restr // LgV//. have Qx2 := s1 _ Qx. have Qx3:= (HJm ljk Qx2). have Px4: inc (P (rep x)) (Vg (isE (ex6_systemi k)) (Q (rep x))). by rewrite (proj41 (ex6_prop5b kL)) LgV//. rewrite xv (inl_restr_cf_ev _ Qx Px2) (ex6_prop6b ljk). rewrite (inl_restr_cf_ev _ Qx2 Px4). by rewrite - (ex6_prop6b lij) (ex6_prop6b lik) inl_restr_cf_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)