proposition: Lemma orsum2_wor r r': worder r -> worder r' -> worder (order_sum2 r r').
proof: Proof. move: cdo_wor => [pa pb] wor wor'; apply: orsum_wor; first by aw. by hnf;aw;move=> i ind; try_lvariant ind. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)