proposition: Lemma ex6_prop4 i:inc i L -> sub_right_directed (Vg Jf i) (isr S).
proof: Proof. rewrite rS;move => iL;split; last by apply: HJrd. by rewrite HIs; apply: ex6_prop1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)