proposition: Lemma inl_restr_canonical_comp S J J' (H: sub_right_directed J (isr S)) (S' := inl_restr H) (H': sub_right_directed J' (isr S')) (g1 := inl_restr_cf H)(g2 := inl_restr_cf H') (g3 := inl_restr_cf (sub_right_directed_trans (is_preorder_r S) H H')): g1 \coP g2 /\ g3 = g1 \co g2.
proof: Proof. move: (inl_restr_cf_compat2 H) => [fg1 sg1 tg1]. move: (inl_restr_cf_compat2 H') => [fg2 sg2 tg2]. have res1: g1 \coP g2 by split => //; rewrite sg1 tg2. have res: function (g1 \co g2) by fct_tac. split => //. rewrite /g3; set H'':=sub_right_directed_trans _ _ _. move: (inl_restr_cf_compat2 H'') => [fg3 sg3 tg3]. have jj: sub J' J by move: (proj1 H'); rewrite is_substrate_r. have rr: sub (induced_order (isr S) J') (induced_order (isr S) J). by move => t /setI2_P [qa qb]; apply/setI2_P;split => //; apply:(setX_Sll jj). have same_data:inl_same_data (inl_restr H'') (inl_restr H'). by rewrite /inl_same_data /= (iorder_trans _ jj) ! double_restr. have sg3sg2:source (inl_restr_cf H'') = source g2. by rewrite sg3 sg2; apply: inductive_limit_Iv. have se:(inl_equiv (inl_restr H'')) = (inl_equiv (inl_restr H')). by apply: inl_equiv_Iv. apply: function_exten => //;aw;trivial; try ue. rewrite sg3sg2 => t ti; rewrite compfV //. move: ti; rewrite sg2 => /inductive_limit_hi [Qj' PE ->]. simpl in Qj', PE. have Qj: inc (Q (rep t)) J by apply:jj. move: PE; rewrite ! LgV// => PE. have PE': inc (P (rep t)) (Vg (isE S') (Q (rep t))) by rewrite /= LgV. rewrite (inl_restr_cf_ev _ Qj' PE') (inl_restr_cf_ev _ Qj PE). by rewrite - se inl_restr_cf_ev. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)