proposition: Lemma orsum2_totalorder r r': total_order r -> total_order r' -> total_order (order_sum2 r r').
proof: Proof. have [ha hb] := cdo_wor. have hc:= (worder_total ha). have hd := proj1 ha. move => pa pb; move:(pa)(pb) => [oa _][ob _]; apply: orsum_total => //. hnf; split => //; [ by aw | by hnf; aw => x xi; try_lvariant xi]. by hnf;aw => x xi; try_lvariant xi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)