proposition: Lemma oprod_rec_def a b: ordinalp a -> ordinalp b -> a *o b = fun_image (a\times b) (fun z => a *o (Q z) +o (P z)).
proof: Proof. move => oa; move: b; apply: least_ordinal2' => c oc prc. set r := (order_prod2 (ordinal_o a) (ordinal_o c)). have woc:worder r by apply: orprod2_wor; apply: ordinal_o_wor. move: (sub_osr a) (sub_osr c) => [ora sra][orc src]. pose f x := a *o (Vg x C0) +o (Vg x C1). have sr: substrate r = product2 c a by rewrite /r orprod2_sr // sra src. suff h: forall x, inc x (substrate r) -> f x = fun_image (segment r x) f. move:(ordinal_isomorphism_exists woc); rewrite -/(ordinal _) -/(a *o c). move => [o1 o2 [[[fuf _] bf] sf tf] sif]; rewrite ordinal_o_sr in tf. rewrite - tf; set_extens w => wt. move /(proj2 bf):wt; rewrite sf; move => [p ps ->]; apply /funI_P. move:(transdef_tg3 woc h ps) => <-. move: ps; rewrite sr => /setX2_P [fp dp vpa vpb]. by exists (J (Vg p C1) (Vg p C0)); [ fprops | aw]. move /funI_P: wt => [z /setX_P [pz pza qzb] ->]. set x := variantLc (Q z) (P z). have xsr: inc x (substrate r). rewrite sr; rewrite /x;apply /setX2_P; split => //;aww. move: (transdef_tg3 woc h xsr). rewrite /f {1 2}/x; aw => ->;Wtac. move => x; rewrite sr => /setX2_P [fp dp vpa vpb]; rewrite /f. set u := (Vg x C0); set v := (Vg x C1). have ou:=(Os_ordinal oc vpa). have ov:=(Os_ordinal oa vpb). rewrite (osum_rec_def (OS_prod2 oa ou) ov). set_extens t. have xca:inc x (product2 c a) by apply/setX2_P. case/setU2_P. rewrite (prc _ vpa); move =>/funI_P [z /setX_P[p za zb] ->]. apply /funI_P; exists (variantLc (Q z) (P z)); aw; trivial. move: (Os_ordinal ou zb)=> oqz. have sa: Q z <> Vg x C0. by move => s;apply: (ordinal_irreflexive oqz); rewrite {2} s. have qzc:=(ordinal_transitive oc vpa zb). apply/segmentP; split; last first. by move => sv; move: (f_equal (Vg ^~C0) sv); aw. apply/(orprod2_gleP ora orc); rewrite sra src; split => //. + apply/setX2_P; split => //; aww. + right; aw; split => //; apply /ordo_leP; split => //. apply: (ordinal_transitive ou zb). move => /funI_P [z za ->];apply /funI_P; exists (variantLc u z); aw; trivial. have iza:=(ordinal_transitive oa vpb za). apply/segmentP; split; last first. move => sv; move: (f_equal (Vg ^~C1) sv); aw. by move => s;apply: (ordinal_irreflexive ov); rewrite -{1} s. apply/(orprod2_gleP ora orc); rewrite sra src; split => //. + apply/setX2_P; split => //; aww. + left;aw; split => //; apply /ordo_leP; split => //. apply: (ordinal_transitive ov za). move => /funI_P [z /segmentP[/(orprod2_gleP ora orc) za zb] ->] . move: za; rewrite sra src; move => [/setX2_P [z1 z2 z3 z4] _]; case. move => [sv /ordo_leP [z5 z6 z7]]; apply /setU2_P; right. apply/funI_P; rewrite sv; exists (Vg z C1) => //. case: (ordinal_sub (Os_ordinal oa z4) ov z7) => //h ; case: zb. by apply: fgraph_exten => //; [ue | rewrite z2 => uu; move /C2_P; case => ->]. move => [/ordo_leP [z5 z6 z7] sv]; apply /setU2_P; left. rewrite (prc _ vpa); apply /funI_P; exists (J (Vg z C1) (Vg z C0)); aw; trivial. move: (Os_ordinal oc z3)(Os_ordinal oc z5) => o1 o2. by apply :setXp_i => //; apply /oltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)