proposition: Lemma opow_prod: forall a b c, ordinalp a -> ordinalp b -> ordinalp c -> a ^o (b *o c) = (a ^o b) ^o c.
proof: Proof. move=> a b c oa ob oc. case: (equal_or_not b \0o) => bz. by rewrite bz (oprod0l) (opowx0 a) (opow1x c). case: (equal_or_not c \0o) => cz. by rewrite cz (oprod0r) !opowx0. have b1:= (ord_ne0_pos ob bz). have c1:= (ord_ne0_pos oc cz). case: (ord2_trichotomy oa) => az. rewrite az (opow0x bz) (opow0x cz) opow0x //. by apply: oprod2_nz. rewrite az (opow1x b) (opow1x c)(opow1x (b *o c)) //. move: (ord_induction_p19 (erefl opow') ord_pow_axioms az b1 c1). rewrite (opow2x b az)(opow2x (b *o c) az). suff: (\2o <=o (opow' a b)) by move => f2; rewrite (opow2x c f2) //. apply: (ord_induction_p41 (erefl opow') _ az b1). by move: ord_pow_axioms => [[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)