proposition: Lemma ord_negl_prod a b c: ordinalp a -> ordinalp b -> \0o <o c -> a <<o b -> a <<o (b *o c).
proof: Proof. move=> oa ob cnz lab. move: (ord_rev_pred cnz) => [oy ->]. rewrite (oprodD OS1 oy ob) (oprod1r ob). apply: ord_negl_sum; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)