proposition: Lemma osum_rec_def a b: ordinalp a -> ordinalp b -> a +o b = a \cup fun_image b (osum2 a).
proof: Proof. move => oa; move: b; apply: least_ordinal2' => c oc prc. set r := (order_sum2 (ordinal_o a) (ordinal_o c)). have woc:worder r by apply: orsum2_wor; apply: ordinal_o_wor. move: (sub_osr a) (sub_osr c) => [ora sra][orc src]. move: C1_ne_C0 C0_ne_C1 => ha hb. pose f x := Yo (Q x = C0) (P x) (a +o (P x)). have sr: substrate r = canonical_du2 a c by rewrite /r orsum2_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=> [/(proj2 bf) | /setU2_P[wt1 | /funI_P [z zc ->]]]. - rewrite sf; move => [p ps ->]; apply /setU2_P. rewrite -(transdef_tg3 woc h ps). move: ps; rewrite sr => /candu2P [pp hh]. rewrite /f; case: hh => [] [p1 ->]; Ytac0;first by left. right;apply/funI_P; ex_tac. - have xsr: inc (J w C0) (substrate r) by rewrite sr; apply: candu2_pra. move: (transdef_tg3 woc h xsr). rewrite /f; aw; Ytac0 => ->; Wtac. - have xsr: inc (J z C1) (substrate r) by rewrite sr; apply: candu2_prb. move: (transdef_tg3 woc h xsr). rewrite /f; aw; Ytac0 => ->;Wtac. move => x; rewrite sr =>/candu2P [px]; case=> [][Px Qx]; rewrite /f. Ytac0; set_extens t. move => tp; apply /funI_P; exists (J t C0); last by aw; Ytac0. move: (ordinal_transitive oa Px tp)(Os_ordinal oa Px) => ta opx. apply /segmentP; split. apply /orsum2_gleP; rewrite sra src; split => //. + by apply: candu2_pra. + by rewrite - px Qx; apply: candu2_pra. + constructor 1; saw => //; apply /ordo_leP; split => //. apply: (ordinal_transitive opx tp). by move => h;case: (ordinal_irreflexive opx); rewrite -{1} h; aw. move => /funI_P [z /segmentP [/orsum2_gleP s1 nzx] ->]. move: s1; rewrite sra src; aw;move => [/candu2P [pz _] _]; case. + move => [q1 _ /ordo_leP [q5 q6 q7]]; Ytac0. case: (ordinal_sub (Os_ordinal oa q5) (Os_ordinal oa q6) q7) => //. move => sp; case: nzx; apply: pair_exten => //;ue. + by move => [_]; case. + by move => [_]; case. rewrite Qx; Ytac0; rewrite (prc _ Px);set_extens t. case /setU2_P. move => ta; apply /funI_P; exists (J t C0); last by aw; Ytac0. apply /segmentP; split; last by move => e; case: ha; rewrite - Qx -e; aw. apply /orsum2_gleP; rewrite sra src; split => //. + by apply: candu2_pra. + by apply /candu2P; split => //;right. + by constructor 3; rewrite Qx;aw. move => /funI_P [z zp ->];apply /funI_P; exists (J z C1); last by aw; Ytac0. move: (ordinal_transitive oc Px zp)(Os_ordinal oc Px) => ta opx. apply /segmentP; split; last first. by move => h;case: (ordinal_irreflexive opx); rewrite -{1} h; aw. apply /orsum2_gleP; rewrite sra src; split => //. + by apply: candu2_prb. + by apply /candu2P; split => //;right. + constructor 2; rewrite Qx;aw; split => //; apply /ordo_leP; split => //. exact: (ordinal_transitive opx zp). move /funI_P => [z /segmentP [/orsum2_gleP s1 s2] ->]. move: s1; rewrite sra src; aw;move => [/candu2P [pz p4] _ p5]; case: p4. by move => [Pz Qz]; Ytac0; apply /setU2_P; left. move => [Pz Qz]; rewrite Qz; Ytac0; case: p5; rewrite Qz; move => [] //. move => _ _ /ordo_leP [_ _ h3]; apply /setU2_P; right; apply /funI_P. exists (P z) => //. case: (ordinal_sub (Os_ordinal oc Pz) (Os_ordinal oc Px) h3) => //. move => e; case: s2; apply: pair_exten => //;ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)