proposition: Lemma oprod2_nc (a := \2o) (b := omega0): a *o b <> b *o a.
proof: Proof. rewrite (oprod_int_omega olt_2omega olt_02) (ord_double OS_omega) => /esym h. move: (osum2_a_ab OS_omega OS_omega h); apply: omega_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)