proposition: Lemma orprod2_wor r r': worder r -> worder r' -> worder (order_prod2 r r').
proof: Proof. move: cdo_wor => [pa pb] wor wor'; apply: orprod_wor => //. - saw. - by hnf; aw; move=> i ind; try_lvariant ind. - apply: finite_set_scdo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)