proposition: Lemma orsum_total1: total_order (order_sum r g) -> (total_order r /\ forall i, inc i (domain g) -> total_order (Vg g i)).
proof: Proof. rewrite /total_order. move: (oa) => [or sr alo];rewrite orsum_sr // sr. move=> [ors to]; split. split => // x y xdg ydg. move: (oa2 xdg) (oa2 ydg) => [a asx][b bsy]. case: (to _ _ (disjoint_union_pi1 xdg asx) (disjoint_union_pi1 ydg bsy)); move=> h; move: (orsum_gle2 h); rewrite /glt. move => aux;left; case: aux; move=> [res _] //; rewrite res; order_tac; ue. move => aux;right; case: aux; move=> [res _] //; rewrite res; order_tac; ue. move=> i idg; move: (alo _ idg) => lo; split => // => x y xsr ysr; red. by case: (to _ _ (disjoint_union_pi1 idg xsr) (disjoint_union_pi1 idg ysr)); move=> h; move: (orsum_gle2 h); case; case => // _ ok; [left | right]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)