proposition: Lemma prl_r3_pr4 i j k: gle prl_r3_nr i j -> gle prl_r3_nr j k -> prl_r3_gij (J i j) \co prl_r3_gij (J j k) = prl_r3_gij (J i k).
proof: Proof. move => lij ljk. have lik:= prl_r3_trans lij ljk. move:(prl_r3_res2 lij) => [fij sij tij]. move:(prl_r3_res2 lik) => [fik sik tik]. move:(prl_r3_res2 ljk) => [fjk sjk tjk]. have cop: prl_r3_gij (J i j) \coP prl_r3_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:(prl_r3_prop7 lij)(prl_r3_prop7 lik)(prl_r3_prop7 ljk) => aij aik ajk. have xs': inc x (source (prl_r3_gij (J j k))) by rewrite sjk. rewrite compfV// /prl_r3_gij; aw. have suij: sub i j by case/sub_gleP:lij. rewrite (LfV ajk s) !LfV // ? double_restr //;exact: (ajk _ s). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)