proposition: Lemma opow_sum a b c: ordinalp a -> ordinalp b -> ordinalp c -> a ^o (b +o c) = (a ^o b) *o (a ^o c).
proof: Proof. move=> oa ob oc. case: (ozero_dichot ob) => bz. rewrite bz opowx0 (osum0l oc) (oprod1l) => //; fprops. case: (ozero_dichot oc) => cz. rewrite cz opowx0 (osum0r ob) (oprod1r) => //; fprops. case: (ord2_trichotomy oa) => az. - rewrite az (opow0x' bz) (opow0x' cz) opow0x. rewrite oprod0r => //; fprops. by move=> sz; move: (osum_Mle0 ob oc); rewrite sz => /(oltNge bz). - rewrite az (opow1x b) (opow1x c)(opow1x (b +o c)). rewrite oprod1r //; fprops. - move: (ord_induction_p18 (erefl opow') ord_pow_axioms az bz cz). rewrite (opow2x b az)(opow2x c az) (opow2x (b +o c) az) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)