proposition: Lemma oprod2_nz a b: ordinalp a -> ordinalp b -> a <> \0o -> b <> \0o -> a *o b <> \0o.
proof: Proof. move=> oa ob anz bnz. exact:(nesym (proj2(oprod2_pos (ord_ne0_pos oa anz) (ord_ne0_pos ob bnz)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)