proposition: Lemma ord_eps_p2_bis a b c (x := oopow a *o b +o c): ordinalp a -> \0o <o b -> ordinalp c -> x <o epsilon0 -> a <o x.
proof: Proof. move => pa pb pc pd. move:(ord_eps_p2 pa pb pc); rewrite -/x; move => [sa sb]; split => // eax. move: (sb (esym eax)) => [_ _ h]. move: (proj2(epsilon_fct_pr3)); rewrite -epsilon_fam_pr2 -/epsilon0 => ha. case: (oltNge pd (ha _ h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)