proposition: Lemma oprod2_one a b: ordinalp a -> ordinalp b -> a *o b = \1o -> (a = \1o /\ b = \1o).
proof: Proof. move=> oa ob ab1. case: (equal_or_not a \1o) => a1. by move: ab1; rewrite a1 oprod1l. case: (equal_or_not b \0c) => bz. by move: ab1; rewrite bz (oprod0r) => bad; case: card1_nz. move: (ord_ne0_pos ob bz) => b1. move: (oprod_Mle1 oa b1); rewrite ab1 => la2. by move: ab1; rewrite (olt1 (conj la2 a1)) oprod0l => bad; case:card1_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)