proposition: Lemma ex1_pr4 i j k: gle rL i j -> gle rL j k -> ex1_gij (J i j) \co ex1_gij (J j k) = ex1_gij (J i k).
proof: Proof. move => lij ljk; move: (proj33 HLp _ _ _ lij ljk) => lik. move:(ex1_res2 lij) => [fij sij tij]. move:(ex1_res2 lik) => [fik sik tik]. move:(ex1_res2 ljk) => [fjk sjk tjk]. have cop: ex1_gij (J i j) \coP ex1_gij (J j k). by split => //; rewrite sij tjk. apply:function_exten. - by apply:compf_f. - exact. - by aw; rewrite sjk sik. - by aw; rewrite tij tik. - aw; rewrite sjk => x s. move:(ex1_prop7 lij)(ex1_prop7 lik)(ex1_prop7 ljk) => aij aik ajk. have xs': inc x (source (ex1_gij (J j k))) by rewrite sjk. rewrite compfV// /ex1_gij; aw; rewrite ! LfV//. by rewrite (double_restr _ (HJm lij)). aw; apply: ajk; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)