proposition: Lemma oprodD a b c: ordinalp a -> ordinalp b -> ordinalp c -> c *o (a +o b) = (c *o a) +o (c *o b).
proof: Proof. move => oa ob oc; move: b ob; apply:least_ordinal2' => d od H. move: (OS_prod2 oc oa) (OS_prod2 oc od) => oca ocd. rewrite (oprod_rec_def oc (OS_sum2 oa od)) (osum_rec_def oa od). rewrite (osum_rec_def oca ocd) {1}(oprod_rec_def oc oa)(oprod_rec_def oc od). set_extens t. move/funI_P => [z /setX_P[pz Pz /setU2_P Qz] ->];case: Qz => h; apply/setU2_P. left; apply /funI_P; exists (J (P z) (Q z)); aww. right; move/funI_P:h => [u ud ->]; rewrite (H _ ud). rewrite - (osumA oca (OS_prod2 oc (Os_ordinal od ud)) (Os_ordinal oc Pz)). apply/funI_P; exists (c *o u +o P z) => //; apply/funI_P. exists (J (P z) u); aww. case /setU2_P; move/funI_P=> [z za ->]; apply/funI_P. move/setX_P: za => [pr pa pb]; exists z => //;apply /setX_P; split;fprops. move/funI_P: za => [w /setX_P [pr pa pb] ->]. rewrite (osumA oca (OS_prod2 oc (Os_ordinal od pb)) (Os_ordinal oc pa)). rewrite - (H _ pb); exists (J (P w) ( a +o Q w)); aw; trivial. apply:setXp_i => //. apply /setU2_P; right; apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)