proposition: Lemma OT_prod2_pr a b: a *t b = OT_prod canonical_doubleton_order (variantLc b a).
proof: Proof. rewrite /OT_prod2 /OT_prod /order_prod2. by rewrite variantLc_comp. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)