proposition: Lemma noid_inl_equiv_esr: equivalence_on noid_inl_equiv noid_inl_sum.
proof: Proof. split; last by apply: graph_on_sr; apply:noid_inl_equiv_reflexive. have ->: noid_inl_equiv = graph_on (fun a b => [/\ inc a noid_inl_sum, inc b noid_inl_sum & noid_inl_equiv_rel a b]) noid_inl_sum. 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 substrate_r => kI lI. move:(directed_r kI lI) => [i [ iI lki lli]]. exists i; split => //. - exact:(proj33 preorder_r _ _ _ lxik lki). - exact:(proj33 preorder_r _ _ _ lzil lli). move/noid_inl_sumP: xE => [_ aI xE]. move/noid_inl_sumP: yE => [_ bI yE]. move/noid_inl_sumP: zE => [_ cI zE]. move: (noid_prop5g lxik lki xE) (noid_prop5g lyik lki yE). rewrite vfxik_yik ; move => -> ->. move: (noid_prop5g lyil lli yE) (noid_prop5g lzil lli zE). by rewrite vfyil_zil; move => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)