proposition: Lemma ord_powa_succ a b: ordinalp a -> ordinalp b -> a ^O (osucc b) = (a ^O b) *o a.
proof: Proof. move => oa ob; rewrite -(osucc_pr ob) (power_of_suma oa ob OS1). by rewrite (ord_powa_pr5 oa) opowx1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)