proposition: Lemma ord_div_nonzero_b a b c: ordinalp a -> ordinalp b -> ordinalp c -> a <o (b *o c) -> b <> \0o.
proof: Proof. move=> oa ob oc ale bz. by move: ale; rewrite bz oprod0l => /olt0. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)