proposition: Lemma orprod2_totalorder r r': total_order r -> total_order r' -> total_order (order_prod2 r r').
proof: Proof. move: cdo_wor => [ha hb]. move => pa pb; move:(pa)(pb) => [oa _][ob _]; apply: orprod_total. 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)