proposition: Lemma osum2_nc (a := \1o) (b := omega0): a +o b <> b +o a.
proof: Proof. rewrite (osum_int_omega olt_1omega) /b=> h. symmetry in h; move: (osum2_a_ab OS_omega OS1 h);apply:card1_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)