proposition: Lemma orprod2_osr: order_on (order_prod2 r r')(product2 (substrate r') (substrate r)).
proof: Proof. have [wor sr] := cdo_wor. have aux: orprod_ax canonical_doubleton_order (variantLc r' r). by split => //; aw; fprops. split; first by apply: orprod_or. rewrite /order_prod2 orprod_sr // /prod_of_substrates canonical2_substrate //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)