proposition: Lemma ord_powa_M_eqle a b c: ordinalp a -> b <=o c -> a <> \0o -> a ^O b <=o a ^O c.
proof: Proof. move => oa bc anz. move: (odiff_pr bc); set d := c -o b; move => [od ->]. rewrite (power_of_suma oa (proj31 bc) od). apply: oprod_Mle1; first by exact (OS_ord_powa oa (proj31 bc)). suff h: a ^O d <> \0o. exact (ord_ne0_pos (OS_ord_powa oa od) h). move => h. move: (ordinal_o_wor oa)(ordinal_o_wor od) => woa wod. move: (ordinal0_pr2 (olexp_worder woa wod) h). have ne: nonempty (substrate (ordinal_o a)). rewrite (ordinal_o_sr a); case: (emptyset_dichot a) => //. move: (olexp_G_least woa wod ne). set m := cst_graph _ _; move => [ms _] bad; empty_tac1 m. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)