proposition: Lemma oprod_int_omega n: n <o omega0 -> \0c <o n -> n *o omega0 = omega0.
proof: Proof. move => no np; move: (no) => [[on oo son] _]. set_extens t; last by apply: (proj33 (oprod_M1le np oo)). rewrite (oprod_rec_def on oo) => /funI_P [z /setX_P [z1 z2 /(oltP oo) z3] ->]. apply /(oltP oo) /(osum2_lt_omega). by apply (oprod2_lt_omega no z3). by apply/(oltP oo); apply: son. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)