proposition: Lemma ord_div_nonzero_b_bis a b: ordinalp a -> \0o <o b -> exists2 c, ordinalp c & a <o (b *o c).
proof: Proof. move=> oa bp. move: (oprod_M1le bp (OS_succ oa)) (oltS oa);rewrite -(osucc_pr oa) => p1 p2. exists (a +o \1o); [ exact (proj32_1 p2) | exact (olt_leT p2 p1) ]. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)