proposition: Lemma ord_square_inj a: ordinalp a -> a ^o \2o = (a *o \2o) ^o \2o -> a = \0o.
proof: Proof. move => oa. case: (ozero_dichot oa) => az; first by exact. have s1: osucc \1c = \2o by rewrite osucc_one. have oa2:= (OS_prod2 oa OS2). have e1: forall u, ordinalp u -> u *o u = u ^o \2o. by move=> u ou; rewrite - s1 (opow_succ ou OS1) (opowx1 ou). rewrite - (e1 _ oa) - (e1 _ oa2) => eq. have e2: a = \2o *o (a *o \2o). move: eq; rewrite - (oprodA oa OS2 oa2) => h. exact: (oprod2_simpl oa (OS_prod2 OS2 oa2) az h). have ha:=(oprod_Mle1 oa olt_02). move:(oprod_M1le olt_02 oa2) ; rewrite - e2 => hb. move:(oleA ha hb) =>eq2. by case: card_12; exact: (esym (oprod2_simpl1 OS2 az (esym eq2))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)