proposition: Lemma oprod_limit x y: \0o <o x -> limit_ordinal y -> limit_ordinal (x *o y).
proof: Proof. by move=> ox ly; apply:normal_ofs_limit=> //; apply: oprod_normal. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)