proposition: Lemma ex6_prop5c i j: gle rL i j -> sub_right_directed (Vg Jf i) (isr (ex6_systemi j)).
proof: Proof. move => lij. have [iL jL] := (ex6_prop2 lij). have ha: sub (Vg Jf j) (substrate (isr S)). by move: (ex6_prop1 jL); rewrite is_substrate_r ex6_prop3. rewrite (proj43 (ex6_prop5b jL)). split; first by rewrite (ipreorder_sr (is_preorder_r S) ha); exact: (HJm lij). move => a b aJi bJi. move:(HJrd iL aJi bJi) => [z [za zb zc]]. move: (HJm lij aJi) (HJm lij bJi) (HJm lij za) => aJj bJj zJj. by exists z; split => //;apply/iorder_gleP; split => //; rewrite rS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)