proposition: Lemma odiff_pr_alt a b (c := ordinal (induced_order (ordinal_o b) (b -s a))): a <=o b -> (ordinalp c /\ b = a +o c).
proof: Proof. move => [oa ob ab]. set F:= b -s a. set B := ordinal_o b. have wB: worder B by rewrite /B;fprops. move: (ordinal_o_sr b); rewrite -/B => sB. have Es: sub a (substrate B) by ue. have Fs: sub F (substrate B) by rewrite sB; apply: sub_setC. set r := induced_order B a. set r' := induced_order B F. have wor: worder r by apply: induced_wor. have wor': worder r' by apply: induced_wor. have -> : c = ordinal r' by done. set A:= ordinal r; set C := ordinal r'. have oA: ordinalp A by apply: OS_ordinal. have oC: ordinalp C by apply: OS_ordinal. split; first by exact. have ra : r = ordinal_o a. apply: order_exten; fprops. move => x y; split => le1. move: (iorder_gle3 le1) => [p1 p2]. move: (iorder_gle1 le1) => /ordo_leP [_ _ h]; apply /ordo_leP;split => //. move /ordo_leP: le1 => [pa pb pc]; apply /iorder_gle0P => //. apply /ordo_leP;split;fprops. have <-: A = a by rewrite /A ra; apply: ordinal_o_o. rewrite /A/C - (ordinal_o_o ob). symmetry; apply: orsum_invariant5 => //. have orb: order B by fprops. have or: order r by fprops. have or': order r' by fprops. have sr: substrate r = a by rewrite /r iorder_sr. have sr': substrate r' = F by rewrite /r' iorder_sr. have ta: forall x, inc x (substrate (order_sum2 r r')) -> inc (P x) (substrate B). move=> x; rewrite orsum2_sr // => /candu2P; rewrite sr sr'. by move=> [_ ]; case; move=> [pqx _]; [apply: Es |apply: Fs]. exists (Lf P (substrate (order_sum2 r r')) (substrate B)). have xxa: total_order (order_sum2 r r'). by apply: orsum2_totalorder; apply: worder_total. have xxb:bijection (Lf P (substrate (order_sum2 r r')) (substrate B)). apply: lf_bijective => //. move=> x y;rewrite orsum2_sr //;move /candu2P=> [px h1] /candu2P [py h2] sp. apply: pair_exten =>//. case: h1; case: h2; move=> [Px Qx][Py Qy];rewrite Qx Qy //. by move: Px Py; rewrite sr sr' /F - sp; move /setC_P => []. by move: Px Py; rewrite sr sr' /F - sp => aux; move /setC_P => []. move=> y ysb; case: (inc_or_not y a) => yE. exists (J y C0); last by aw. by rewrite orsum2_sr //; apply candu2_pra; rewrite sr. have yF: inc y F by rewrite /F - sB; apply /setC_P; split. exists (J y C1); last by aw. by rewrite orsum2_sr //; apply :candu2_prb; rewrite sr'. apply: total_order_isomorphism => //; aw; trivial. move=> x y xsr ysr /=; rewrite LfV // LfV //. move: xsr ysr; rewrite orsum2_sr //; move=> xsr ysr => ha. move /orsum2_gleP:ha => [_ _ ]; case. by move=> [_ _ h1]; move: (iorder_gle1 h1). by move=> [_ _ h1]; move: (iorder_gle1 h1). move => [qxa qyb]. move: xsr ysr => /candu2P [px h1] /candu2P [py h2]. case: h1; last by move=> [_]; rewrite qxa => aux; case: C0_ne_C1. case: h2; first by move=> [_ xx]; rewrite xx in qyb; case: qyb. rewrite sr sr'; move=> [Py _] [Px _ ]. move: (worder_total wB)=> [_ tob]. have xb: inc (P x) (substrate B) by apply: Es. have yb: inc (P y) (substrate B) by apply: Fs. case: (tob _ _ xb yb) => //. move: Py => /setC_P [_ nya] /ordo_leP [iyb ixb xy]; case: nya. case: (ordinal_sub (Os_ordinal ob iyb) (Os_ordinal ob ixb) xy). by move=> ->. apply: (ordinal_transitive oa Px). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)