proposition: Lemma ord_eps_p2 a b c (x := ((oopow a) *o b) +o c) : ordinalp a -> \0o <o b -> ordinalp c -> (a <=o x /\ (x = a -> [/\ c = \0o, b = \1o & epsilonp x])).
proof: Proof. move=> oa bp oc. have oo:= OS_omega. have ob:= proj32_1 bp. have op:= OS_pow oo oa. have ot:= OS_prod2 op ob. have ox:= (OS_sum2 (OS_prod2 op ob) oc). have le1:= (ord_eps_p1 oa). have le2:= (oprod_Mle1 op bp). have le3:= (osum_Mle0 ot oc). have le4:=(oleT le1 le2). have le5:=(oleT le4 le3). split => // xa; rewrite xa; rewrite -/x in le3. have pa: a = ((oopow a) *o b) by apply: (oleA le4); rewrite - {2} xa. have c0: c = \0c by apply: (osum2_a_ab oa oc); rewrite -{2} xa /x -pa. case: (oone_dichot bp) => b1. by split => //; split => //; rewrite {2} pa b1 oprod1r. by move: (oprod_Meq1lt b1 (oopow_pos oa)); rewrite - pa => /(oleNgt le1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)