proposition: Lemma ex1_preorder i (ri:= induced_order rI (Vg Jf i)): ( forall k, inc k L -> forall i j, inc i (Vg Jf k) -> inc j (Vg Jf k) -> exists t, [/\ inc t (Vg Jf k), gle rI i t & gle rI j t]) -> inc i L -> [/\ preorder ri, substrate ri = (Vg Jf i) & right_directed_prop ri].
proof: Proof. move => h' h. have pa : sub (Vg Jf i) (substrate rI) by rewrite HIs; apply:(ex1_prop1 h). have pb:= (ipreorder_sr HIp pa). have pc:= iorder_preorder pa HIp. split => // a b; rewrite pb => ai bi. move:(h' _ h _ _ ai bi) => [c [ci ca cb]]. by exists c; split; [apply/(iorder_gle0P rI ai ci)|apply/(iorder_gle0P rI bi ci)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)