proposition: Lemma inl_equiv_esr S: equivalence_on (inl_equiv S) (inl_sum S).
proof: Proof. split; last by apply: graph_on_sr; apply:inl_equiv_reflexive. have ->: (inl_equiv S) = graph_on (fun a b => [/\ inc a (inl_sum S), inc b (inl_sum S) & inl_equiv_rel S a b]) (inl_sum S). by apply: Zo_exten1 => t /setX_P [_ px qx]; split => // [] [_ _]. apply: equivalence_from_rel; split. by move => x y [xs ys [k [ha hb hc]]]; split => //;exists k; split. move=> y x z [xE yE [k [lxik lyik vfxik_yik]]] [_ zE [l [lyil lzil vfyil_zil]]]. split => //. move: (arg2_sr lxik)(arg2_sr lyil); rewrite is_substrate_r => kI lI. move:(is_directed_r kI lI) => [i [ iI lki lli]]. exists i; split => //. - exact:(proj33 (is_preorder_r S) _ _ _ lxik lki). - exact:(proj33 (is_preorder_r S) _ _ _ lzil lli). move/inl_sumP: xE => [_ aI xE]. move/inl_sumP: yE => [_ bI yE]. move/inl_sumP: zE => [_ cI zE]. move: (inl_prop3 lxik lki xE) (inl_prop3 lyik lki yE). rewrite vfxik_yik ; move => -> ->. move: (inl_prop3 lyil lli yE) (inl_prop3 lzil lli zE). by rewrite vfyil_zil; move => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)