proposition: Lemma orprod_invariant4 r1 r2 r3 r4: r1 \Is r3 -> r2 \Is r4 -> (order_prod2 r1 r2) \Is (order_prod2 r3 r4).
proof: Proof. move=> h1 h2; rewrite /order_prod2. move:cdo_wor => [pa pb]. by apply: orprod_invariant2; rewrite ? pb ? Lgd // => i itp; try_lvariant itp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)