proposition: Lemma orsum_gle2 a b a' b': gle (order_sum r g) (J a b)(J a' b') -> (glt r b b' \/ (b = b' /\ gle (Vg g b) a a')).
proof: Proof. by move => h2; move:(orsum_gle1 h2); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)