proposition: Lemma osum2_nD (a:= \1o) (b:= \1o) (c:= omega0): (a +o b) *o c <> (a *o c) +o (b *o c).
proof: Proof. rewrite (oprod_int_omega olt_1omega olt_01) (osum2_2int NS1 NS1). rewrite csum_11 (oprod_int_omega olt_2omega olt_02) => /esym h. move: (osum2_a_ab OS_omega OS_omega h). apply: omega_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)