proposition: Lemma oprod2_two a b: ordinalp a -> ordinalp b -> a *o b = \2o -> (a = \1o \/ b = \1o).
proof: Proof. move=> oa ob ab1. case: (equal_or_not b \0c) => bz. by move: ab1; rewrite bz (oprod0r) => bad; case: card2_nz. have b1:= (ord_ne0_pos ob bz). move: (oprod_Mle1 oa b1); rewrite ab1 => la2. case:(ole_eqVlt la2) => a2. by right; apply: (oprod2_simpl ob OS1 olt_02); rewrite -{1}a2 (oprod1r OS2). move: a2; rewrite - osucc_one=>/oltSleP/ole_eqVlt; case; first by left. move/olt1 => az. by move: ab1; rewrite az (oprod0l) => bad; case: card2_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)