proposition: Lemma orsum_g1 i x i' x': inc (J i x) (sum_of_substrates g) -> inc (J i' x') (sum_of_substrates g) -> gle r x x' -> x <> x' -> gle (order_sum r g) (J i x) (J i' x').
proof: Proof. move=> js1 js2 le1 lt1. apply /orsum_gleP; split => //; left; saw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)