proposition: Lemma opow_Mspec2 a b: ordinalp b -> \2o <=o a -> (a *o b) <=o (a ^o b).
proof: Proof. move=> ob oa2. have oa:= proj32 oa2. have a1:=(olt_leT olt_02 oa2). move: (ord2_trichotomy1 oa2) => [pa1 pa2]. move: b ob;apply: least_ordinal2 => t ot lpy. case: (ordinal_limA ot). move => ->;rewrite opowx0 oprod0r; exact: ole_01. move=> [y oy ty]. rewrite ty (opow_succ oa oy) (oprod2_succ oa oy). case: (ozero_dichot oy) => ynz. rewrite ynz oprod0r opowx0 osum0l // oprod1l;fprops. have op:= (OS_pow oa oy). move: (oprod_Mlele (oleR op) oa2). rewrite (ord_double op)=> le1. have lpyc: y <o t by rewrite ty; apply: oltS. move: (lpy _ lpyc)=> le2. have au: a <=o (a ^o y) by apply: opow_Meqle1. exact:(oleT (osum_Mlele le2 au) le1). move=> tl. rewrite (proj2 (oprod_normal a1) _ tl). have pato:= (OS_pow oa ot). apply: ord_ub_sup => //. move=> i /funI_P [z /(oltP ot) zt ->]. apply: (oleT (lpy _ zt));exact:(opow_Meqle a1 (proj1 zt)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)