proposition: Lemma orsum_total r g: orsum_ax r g -> total_order r -> (forall i, inc i (domain g) -> total_order (Vg g i)) -> total_order (order_sum r g).
proof: Proof. move=> oa [_ tor] alt; rewrite /total_order. move: (oa) => [or sr alo]; rewrite orsum_sr //. rewrite sr in tor. split =>//; first by fprops. move=> x y xsr ysr; move: (du_index_pr1 xsr) (du_index_pr1 ysr). move=> [Qx Px px][Qy Py py]. case: (equal_or_not (Q x) (Q y)). move =>h; move: (alt _ Qx) => [lor ltor]; rewrite -h in Py. case: (ltor _ _ Px Py) => h1;aw ; [left | right]; apply /orsum_gleP;split => //; right; split => //; ue. move=> nQ; case: (tor _ _ Qx Qy) => h; [left | right]; apply /orsum_gleP;split => //; left;split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)