proposition: Lemma orsum_gle_id x x': gle (order_sum r g) x x' -> gle r (Q x) (Q x').
proof: Proof. move /orsum_gleP => [xs _ ] [] [] => // <- _. move: (du_index_pr1 xs)=> [qd _ _]. move: osa => [or srdg _]; order_tac; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)