proposition: Lemma ex7_fij_prop3 i j k: gle (isr S) i j -> gle (isr S) j k -> ex7_fij j k \co ex7_fij i j = ex7_fij i k.
proof: Proof. move => lij ljk. move:(proj33(is_preorder_r S) _ _ _ lij ljk) => lik. move:(ex7_fij_prop1 lij) => [fij sij tij]. move:(ex7_fij_prop1 lik) => [fik sik tik]. move:(ex7_fij_prop1 ljk) => [fjk sjk tjk]. have co: ex7_fij j k \coP ex7_fij i j by split => //;ue. apply: function_exten; aw=> //; try ue; first by fct_tac. rewrite sij => x xEi. have ha: inc x (source (ex7_fij i j)) by ue. have hb: inc (Vf (ex7_fij i j) x) (ex7_Ei j) by Wtac. rewrite compfV //. rewrite (ex7_fij_ev lik xEi)(ex7_fij_ev ljk hb)(ex7_fij_ev lij xEi). clear fij sij tij fik sik tik fjk sjk tjk ha hb co. move:(inl_prop0 lij)(inl_prop0 ljk) => [iI jI][_ kI]. move:(ex7_eqv_prop1 iI) => [eqRi sRi]. move:(ex7_eqv_prop1 jI) => [eqRj sRj]. move:(ex7_eqv_prop1 kI) => [eqRk sRk]. move: (rep_i_sr eqRi xEi); rewrite sRi => rE. move:(inl_prop4 lij) => [fij sij tij]. move:(inl_prop4 lik) => [fik sik tik]. move:(inl_prop4 ljk) => [fjk sjk tjk]. have fre: inc (Vf (Vg (isf S) (J i j)) (rep x)) (substrate (ex7_eqv j)). rewrite sRj; Wtac. move: (related_rep_class eqRj fre); set y := rep (class _ _). move/(ex7_eqv_prop2 jI) => [];set z := Vf _ _ => zEj yEj rzy. apply:(class_eq1 eqRk); apply/(ex7_eqv_prop2 kI); split; try Wtac. by rewrite inl_class_of_fij // inl_class_of_fij // - rzy /z inl_class_of_fij. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)