proposition: Lemma oprodA a b c: ordinalp a -> ordinalp b -> ordinalp c -> a *o (b *o c) = (a *o b) *o c.
proof: Proof. move => oa ob; move: c; apply: least_ordinal2' => d od H. rewrite (oprod_rec_def oa (OS_prod2 ob od)) (oprod_rec_def ob od). rewrite (oprod_rec_def (OS_prod2 oa ob) od) {1} (oprod_rec_def oa ob). set_extens t; case /funI_P => [z za ->]; apply /funI_P. move /setX_P:za=> [pz p1z /funI_P [u /setX_P [ppz p2z p3z] ->]]. move:(Os_ordinal ob p2z)(Os_ordinal od p3z)(Os_ordinal oa p1z)=> opu oqu opz. have obqu:= (OS_prod2 ob oqu). rewrite (oprodD obqu opu oa). rewrite - (osumA (OS_prod2 oa obqu) (OS_prod2 oa opu)opz) (H _ p3z). exists (J (a *o P u +o P z) (Q u)); aw;trivial;apply: setXp_i => //. by apply/funI_P; exists (J (P z) (P u)); aw;trivial;apply: setXp_i. move /setX_P:za=> [pz /funI_P [u /setX_P [pu p1 p2] ->] qzd]. move:(Os_ordinal oa p1)(Os_ordinal ob p2)(Os_ordinal od qzd)=> opu oqu oqz. rewrite (osumA (OS_prod2 (OS_prod2 oa ob) oqz) (OS_prod2 oa oqu) opu). rewrite -(H _ qzd) - (oprodD (OS_prod2 ob oqz) oqu oa). exists (J (P u) (b *o Q z +o Q u)); aw; trivial;apply: setXp_i => //. by apply /funI_P;exists (J (Q u) (Q z)); aw; trivial;apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)