Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset11.

Module Ordinals2.

Definition ord_sub b a :=
  ordinal (induced_order (ordinal_o b) (complement b a)).

Notation "x -o y" := (ord_sub x y) (at level 50).

Lemma ord_sub_pr: forall a b, a <=o b
  -> (is_ordinal (b -o a) & b = a +o (b -o a)).
move=> a b; rewrite ordinal_le_pr0;move => [oa [ob ab]].
set F:= complement b a.
set B := ordinal_o b.
have wB: worder B by apply ordinal_worder2.
move: (ordinal_p7 ob); rewrite -/B => sB.
have Es: sub a (substrate B) by ue.
have Fs: sub F (substrate B) by rewrite sB; apply sub_complement.
set r := induced_order B a.
set r' := induced_order B F.
have wor: worder r by apply worder_restriction.
have wor': worder r' by apply worder_restriction.
have -> : (ord_sub b a) = ordinal r' by done.
set A:= ordinal r; set C := ordinal r'.
have oA: is_ordinal A by apply ordinal_p1.
have oC: is_ordinal C by apply ordinal_p1.
split; first by exact.
have ra : r = ordinal_o a.
  have gr: is_graph r by apply (order_is_graph (worder_is_order wor)).
  have ga: is_graph (ordinal_o a). apply order_is_graph. fprops.
  rewrite graph_exten => //.
  move=> u v; aw; rewrite /r/B; apply iff_eq.
    move=> rr; move: (iorder_gle3 rr) => [p1 p2]; ee.
    move: (iorder_gle1 rr); aw; intuition.
  move=> [p1 [p2 p3]]; aw; ee.
have <-: A = a by rewrite /A ra; apply ordinal_p3.
rewrite /A/C - (ordinal_p3 ob).
symmetry; apply ord_sum_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; aw.
have sr': substrate r' = F by rewrite /r'; aw.
have ta: forall x, inc x (substrate (order_sum2 r r'))
   -> inc (P x) (substrate B).
  move=> x; rewrite order_sum2_substrate // canonical_du2_pr sr sr'.
  by aw; move=> [_ ]; case; move=> [pqx _]; [apply Es |apply Fs].
exists (BL P (substrate (order_sum2 r r')) (substrate B)).
apply total_order_isomorphism => //; aw.
- by apply order_sum2_totalorder; apply worder_total.
- apply bl_bijective => //.
    move=> x y;rewrite order_sum2_substrate // ! canonical_du2_pr //.
    move=> [px h1][py h2] sp; apply pair_exten =>//.
    case h1; case h2; move=> [Px Qx][Py Qy]; rewrite Qx Qy //;
      move: Px Py; rewrite sr sr' /F -sp; srw; intuition.
  move=> y ysb; case (inc_or_not y a) => yE.
    exists (J y TPa); rewrite order_sum2_substrate //canonical_du2_pr //.
    rewrite sr; aw; ee.
  have yF: inc y F by rewrite /F -sB; srw; ee.
  exists (J y TPb); rewrite order_sum2_substrate //canonical_du2_pr //.
  rewrite sr';aw; ee.
- done.
  move=> x y xsr ysr; rewrite bl_W// bl_W //.
  move: xsr ysr; rewrite order_sum2_substrate //; move=> xsr ysr.
  rewrite order_sum2_gle // /r/r'.
  move=>[_ [_ h]]; case h.
    by move=> [_ [_ h1]]; move: (iorder_gle1 h1).
  case; first by move=> [_ [_ h1]]; move: (iorder_gle1 h1).
  move => [qxa qyb].
  move: xsr ysr; rewrite ! canonical_du2_pr //; move=> [px h1][py h2].
  case h1; last by move=> [_]; rewrite qxa => aux; elim two_points_distinct.
  case h2; first by move=> [_ xx]; rewrite xx in qyb; elim 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; rewrite /F; srw; rewrite /gge /B; aw.
  move=> [_ nya] [iyb [ixb xy]]; elim nya.
  case (ordinal_sub (elt_of_ordinal ob iyb) (elt_of_ordinal ob ixb) xy).
    by move=> ->.
  apply (ordinal_transitive oa Px).
Qed.

Lemma ord_plus_simp_left: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  c +o a = c +o b -> a = b.
Proof.
move=> a b c oa ob oc so.
case : (ordinal_le_total_order1 oa ob) => h.
  move: (ord_sub_pr h) => [occ os].
  move: so; rewrite os order_sum_assoc3//; move => aux.
  move: (ordinal_a_ne_ab (ord_sum2_ordinal oc oa) occ aux).
  move=> ->; rewrite ord_0_plus_unit_r //; apply ordinal_pr10 => //.
move: h => [h1 _].
move: (ord_sub_pr h1) => [occ os].
move: so; rewrite os order_sum_assoc3 //; move=> aux; symmetry in aux.
move: (ordinal_a_ne_ab (ord_sum2_ordinal oc ob) occ aux).
move=> ->; rewrite ord_0_plus_unit_r //; apply ordinal_pr10 => //.
Qed.

Lemma ord_sub_pr1: forall a b,
   is_ordinal a -> is_ordinal b ->
   (a +o b) -o a = b.
Proof.
move=> a b oa ob.
have p:ordinal_le a (ord_sum2 a b) by apply ord_sum2_increasing2.
move: (ord_sub_pr p)=> [so sp].
by symmetry; apply (ord_plus_simp_left ob so oa).
Qed.

Lemma ord_sub_smaller: forall a b, a <=o b -> (b -o a) <=o b.
Proof.
move=> a b leab; move: (ord_sub_pr leab) => [os op].
move: leab => [oa _].
rewrite {2} op; apply ord_sum2_increasing3 =>//.
Qed.

Lemma ord_plus_compat_lt: forall a b c,
  a <o b -> is_ordinal c -> (c +o a) <o (c +o b).
Proof.
move=> a b c [leab neab] oc; split.
  apply ord_sum2_increasing1 =>//; ord_tac.
move: leab => [oa [ob _]];dneg ab; apply ord_plus_simp_left with c =>//.
Qed.

Lemma ord_mult_compat_lt: forall a b c,
  a <o b -> is_ordinal c -> c <> 0o -> (c *o a) <o (c *o b).
Proof.
move=> a b c ab oc cz; move: (ab)=> [[oa [ob _]] _].
move: ab;rewrite ord_succ_lt2 // => p1.
move: ordinal_1 => oo.
have: ordinal_le (ord_prod2 c (succ_o a)) (ord_prod2 c b).
    apply ord_prod2_increasing1 => //; ord_tac.
rewrite -(ord_succ_pr oa).
rewrite order_sum_distributive3// ord_1_mult_unit_r // => le1.
set ca := (ord_prod2 c a).
have cao: is_ordinal ca by apply ord_prod2_ordinal.
have le2: ordinal_lt ca (ord_sum2 ca c).
  split; first by apply ord_sum2_increasing2 => //.
  dneg cac; apply ordinal_a_ne_ab with ca =>//.
ord_tac.
Qed.

Lemma ord_mult_compat_lt1: forall b c,
   is_ordinal c -> is_ordinal b -> c <> 0o ->
   b <> 0o -> b <> 1o -> c <o (c *o b).
Proof.
move => b c oc ob cnz bnz bn1.
have cv: c = (ord_prod2 c 1o) by rewrite ord_1_mult_unit_r //.
have lt1b: ordinal_lt 1o b.
  split; [apply zero_least_ordinal1 => // |intuition ].
rewrite {1} cv.
apply (ord_mult_compat_lt lt1b oc cnz).
Qed.

Lemma ord_mult_simp_left: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c -> c <> 0o ->
  c *o a = c *o b -> a = b.
Proof.
move=> a b c oa ob oc cz so.
ex_middle ab.
case : (ordinal_le_total_order1 oa ob) => h.
  have ltab : ordinal_lt a b by split.
  move: (ord_mult_compat_lt ltab oc cz); rewrite so; move=> [_ bad].
  by elim bad.
move: (ord_mult_compat_lt h oc cz); rewrite so; move=> [_ bad].
by elim bad.
Qed.

Lemma ord_plus_compat_lt1: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  (c +o a) <o (c +o b) -> a <o b.
Proof.
move => a b c oa ob oc olt.
case (ordinal_le_total_order1 ob oa) => //.
move=> oba.
have aux: ordinal_le (ord_sum2 c b) (ord_sum2 c a).
apply ord_sum2_increasing1 => //; ord_tac.
ord_tac.
Qed.

Lemma ord_plus_compat_lt2: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  (a +o c) <o (b +o c) -> a <o b.
Proof.
move => a b c oa ob oc olt.
case (ordinal_le_total_order1 ob oa) => //.
move=> oba.
have aux: ordinal_le (ord_sum2 b c) (ord_sum2 a c).
apply ord_sum2_increasing1 => //; apply ordinal_le_reflexive => //.
elim (ordinal_le_antisymmetry1 aux olt).
Qed.

Lemma ord_prod_compat_lt1: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  (c *o a) <o (c *o b) -> a <o b.
Proof.
move => a b c oa ob oc olt.
case (ordinal_le_total_order1 ob oa) => //.
move=> oba.
have aux: ordinal_le (ord_prod2 c b) (ord_prod2 c a).
apply ord_prod2_increasing1 => //; apply ordinal_le_reflexive => //.
elim (ordinal_le_antisymmetry1 aux olt).
Qed.

Lemma ord_prod_compat_lt2: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  (a *o c) <o (b *o c) -> a <o b.
Proof.
move => a b c oa ob oc olt.
case (ordinal_le_total_order1 ob oa) => //.
move=> oba.
have aux: ordinal_le (ord_prod2 b c) (ord_prod2 a c).
apply ord_prod2_increasing1 => //; apply ordinal_le_reflexive => //.
elim (ordinal_le_antisymmetry1 aux olt).
Qed.


Lemma ord_sup_pr6: forall E, ordinal_set E ->
  greatest_element (graph_on ordinal_le (tack_on E (\osup E)))
    (\osup E).
Proof.
move=> E Ep.
move: (ord_sup_pr2 Ep) => [os _].
have alo: forall x, inc x (tack_on E (union E)) -> ordinal_le x x.
  move=> x; aw; move => xs; apply ordinal_le_reflexive.
  case xs; [apply Ep | move=> ->; exact].
move: (wordering_pr wordering_ordinal_le alo) => [p1 p2].
red; aw; rewrite p1;split; first by fprops.
move => x xt; rewrite /gle graph_on_rw1; split => //; split; fprops.
move: xt; aw; case; first by apply ord_sup_pr3 =>//.
by move => ->; ord_tac.
Qed.

Lemma ord_sup_pr7: forall a, is_ordinal a ->
  let b := \osup a in
    b = a \/ a = succ_o b.
Proof.
move=> a oa b.
move: (limit_ordinal_pr0 oa) => [p1 _].
case p1; last by move=>->; left.
by move=> yp; right; apply ordinal_predecessor1.
Qed.

Lemma ord_sup_pr8: forall X, ordinal_set X ->
  ~ (inc (\osup X) X) ->
  forall x, inc x X -> x <o (\osup X).
Proof.
move=> X h1 h2 x xX; split; first by apply ord_sup_pr3 => //.
by dneg xs; rewrite -xs.
Qed.

Lemma ord_sup_pr9: forall X,
   ordinal_set X -> nonempty X ->
  inc (\osup X) X \/ limit_ordinal (\osup X).
Proof.
move=> X alo [a aX].
move: (ord_sup_pr3 alo aX) => asu.
have so: (is_ordinal (union X)) by move: asu => [_ [ok _]].
case (p_or_not_p (inc (union X) X)) => nsX; first by intuition.
right.
case (limit_ordinal_pr2 so).
  move=> h; rewrite h in nsX asu; rewrite (zero_least_ordinal3 asu) in aX.
  contradiction.
case => //; move=> [y h].
have oy: is_ordinal y.
   have ys: inc y (union X) by rewrite h /succ_o; fprops.
   ord_tac.
have aiy: (forall i, inc i X -> ordinal_le i y).
  move=> i iX;rewrite - ord_lt_succ -h.
  apply ord_sup_pr8 => //.
move: (ord_sup_pr4 alo oy aiy); rewrite h.
by rewrite - ord_succ_lt2; move => [_ bad].
Qed.

Lemma ord_sum_pr10: forall x y, sub x y -> ordinal_set y ->
  (\osup x) <=o (\osup y).
Proof.
move=> x y xy al1.
have al2: ordinal_set x by move=> z zx; apply (al1 _ (xy _ zx)).
apply ord_sup_pr4 => //; first by apply ord_sup_pr1.
by move=> i ix; apply ord_sup_pr3 => //; apply xy.
Qed.

Definition cofinal_ordinal x y :=
   ordinal_set x & ordinal_set y &
   (forall a, inc a x -> exists b, inc b y & a <=o b) &
   (forall a, inc a y -> exists b, inc b x & a <=o b).

Lemma ord_sup_pr11: forall x y, cofinal_ordinal x y ->
  \osup x = \osup y.
Proof.
move=> x y [p1 [p2 [p3 p4]]].
apply ordinal_le_antisymmetric.
  apply ord_sup_pr4 => //.
    apply ord_sup_pr1 => //.
  move=> i ix; move: (p3 _ ix) => [j [jy lij]].
  apply ordinal_le_transitive with j =>//;apply ord_sup_pr3 => //.
apply ord_sup_pr4 => //.
  apply ord_sup_pr1 => //.
move=> i ix; move: (p4 _ ix) => [j [jy lij]].
apply ordinal_le_transitive with j =>//;apply ord_sup_pr3 => //.
Qed.

Lemma ord_sup_pr12: forall X f g,
  (forall x, inc x X -> f x = g x) ->
  \osup (fun_image X f) = \osup (fun_image X g).
Proof.
move=> X f g h.
have->: (fun_image X f = fun_image X g).
   set_extens t; aw; move=> [z [zX]] <-; ex_tac.
   by symmetry; apply h.
done.
Qed.

Lemma ord_sup_pr13: forall x y,
  sub x y -> ordinal_set y ->
  (forall a, inc a y -> exists b, inc b x & a <=o b) ->
  \osup x = \osup y.
Proof.
move=> x y h1 h2 h3; apply ord_sup_pr11; red; ee.
  move=> t tx; apply (h2 _ (h1 _ tx)).
move=> a ay; exists a;ee.
move:(h2 _ (h1 _ ay)) => ox; ord_tac.
Qed.

Lemma ordinal_not_collectivizing: forall E,
   (forall x, is_ordinal x -> inc x E) -> False.
Proof.
move=> E Ep.
set F := Zo E (fun z => is_ordinal z).
have Fp1: forall z, inc z F -> is_ordinal z.
  by move=> z; rewrite Z_rw; intuition.
move:(ord_sup_pr3 Fp1).
move:(ord_sup_pr2 Fp1) => [oa _].
set a := union F.
move=> Fp2.
have sF:inc (succ_o a) F.
   move: (succ_ordinal oa) => aux.
   rewrite -(ord_succ_pr oa) Z_rw; ee.
move:(Fp2 _ sF)(ord_succ_lt oa).
apply ordinal_le_antisymmetry1.
Qed.

Definition ord_div_pr0 a b q r :=
  is_ordinal q & is_ordinal r & a = (b *o q) +o r & r <o b.

Definition ord_div_pr1 a b c q r :=
  ord_div_pr0 a b q r & q <o c.

Lemma ord_div_nonzero_b: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  a <o (ord_prod2 b c) -> b <> 0o.
Proof.
move=> a b c oa ob oc ale.
move: (zero_least_ordinal1 oa) => oz.
have [_ pz]: ordinal_lt 0o (ord_prod2 b c).
  apply ordinal_le_lt_trans with a => //.
  apply zero_least_ordinal => //.
dneg x; rewrite x ord0_prodl //; apply ordinal_pr10.
Qed.

Lemma ord_div_nonzero_b_bis: forall a b,
  is_ordinal a -> is_ordinal b -> b <> 0o ->
  exists c, is_ordinal c & a <o (b *o c).
Proof.
move=> a b oa ob bnz.
move: (succ_ordinal oa) => os.
move: (ord_prod2_increasing3 ob os bnz).
move: (ord_succ_lt oa);rewrite -(ord_succ_pr oa).
move=> p1 p2; exists (ord_sum2 a 1o).
split; [ exact | apply (ordinal_lt_le_trans p1 p2)].
Qed.

Lemma ord_division_unique: forall a b q r q' r',
  is_ordinal a -> is_ordinal b ->
  ord_div_pr0 a b q r -> ord_div_pr0 a b q' r' ->
  (q = q' & r = r').
Proof.
have aux: forall b q r q' r', is_ordinal b -> is_ordinal q -> is_ordinal r ->
  is_ordinal q' -> is_ordinal r' ->
  ordinal_lt q q' -> ordinal_lt r b ->
  ordinal_lt (ord_sum2 (ord_prod2 b q) r) (ord_sum2 (ord_prod2 b q') r').
  move=> b q r q' r' ob oq or oq' or' lt1 lt2.
  move: lt1;rewrite ord_succ_lt2 // => p1.
  move: ordinal_1 => oo.
  have: ordinal_le (ord_prod2 b (succ_o q)) (ord_prod2 b q').
    apply ord_prod2_increasing1 => //; apply ordinal_le_reflexive => //.
  rewrite -(ord_succ_pr oq) order_sum_distributive3 =>//.
  rewrite ord_1_mult_unit_r //; move => le2.
  move: (ord_plus_compat_lt lt2 (ord_prod2_ordinal ob oq)) => lt3.
  move: (ord_sum2_increasing2 (ord_prod2_ordinal ob oq') or')=> lt4.
  apply (ordinal_lt_le_trans (ordinal_lt_le_trans lt3 le2) lt4).
move=> a b q r q' r' oa ob .
move=> [oq [or [oae ltrb]]] [oq' [or' [oae' ltrb']]].
case (equal_or_not q q') => qq'.
  split => //;rewrite oae -qq' in oae'.
  apply ord_plus_simp_left with (ord_prod2 b q) => //.
  apply ord_prod2_ordinal=> //.
case (ordinal_le_total_order1 oq oq') => leqq'.
  have ltqq': ordinal_lt q q' by split.
  move: (aux _ _ _ _ _ ob oq or oq' or' ltqq' ltrb).
  by rewrite - oae - oae' => aa; elim aa.
move: (aux _ _ _ _ _ ob oq' or' oq or leqq' ltrb').
by rewrite - oae - oae' => aa; elim aa.
Qed.

Lemma ord_division_exists: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  ordinal_lt a (ord_prod2 b c) ->
  exists q, exists r, ord_div_pr1 a b c q r.
Proof.
move=> a b c oa ob oc=> a_bc.
rewrite /ord_prod2 in a_bc.
set pbc:= (order_prod2 (ordinal_o b) (ordinal_o c)).
have obc: worder pbc by apply order_prod2_worder; apply ordinal_worder2 => //.
move: (ordinal_lt_pr2 obc a_bc) => [f [x [xsp [rgx om]]]].
have orb: order (ordinal_o b) by apply ordinal_p11.
have orc: order (ordinal_o c) by apply ordinal_p11.
have ora: order (ordinal_o a) by apply ordinal_p11.
move: (xsp); rewrite order_prod2_substrate // product2_rw.
move: (ordinal_p7 ob) (ordinal_p7 oc) => sb sc.
rewrite sb sc.
move=> [fgx [dx [xa xb]]].
have [w [wsb wle]]: exists w, inc w b &
  (forall t, inc t b -> gle (ordinal_o b) w t).
  have nesb: nonempty (substrate (ordinal_o b)) by rewrite sb;ex_tac.
   move: (worder_least (ordinal_worder2 ob) nesb) => [w [p1 p2]].
   rewrite sb in p1 p2; ex_tac.
set y := variantLc (V TPa x) w.
have ysp: inc y (substrate pbc).
  rewrite order_prod2_substrate // product2_rw sb sc /y; bw; ee.
set r := (V TPb x) ; set q := (V TPa x).
have lt_rb: ordinal_lt r b.
  by rewrite ordinal_lt_pr0; ee; apply (elt_of_ordinal ob xb).
have lt_qc: ordinal_lt q c.
  by rewrite ordinal_lt_pr0; ee; apply (elt_of_ordinal oc xa).
have oq: is_ordinal q by move: lt_qc => [[oq _] _].
have odr: is_ordinal r by move: lt_rb => [[odr _] _].
have worr: worder (ordinal_o r) by apply ordinal_worder2.
have orq: order (ordinal_o q) by fprops.
move: (ordinal_p7 oq) => sq.
have sqc: sub q c.
  by move: lt_qc => [h _]; rewrite ordinal_le_pr0 in h; intuition.
have srb: sub r b.
  by move: lt_rb => [h _]; rewrite ordinal_le_pr0 in h; intuition.
exists q; exists r; rewrite /ord_div_pr1 /ord_div_pr0 ; ee.
have rsub: forall r A u v, order r -> sub A (substrate r) ->
  gle (induced_order r A) u v = (inc u A & inc v A & gle r u v).
  move=> r0 A0 u v or Asr; apply iff_eq.
    rewrite /gle/related/induced_order/coarse; aw; intuition.
    move=> [uA [vA rr]]; aw.
set A:= segment pbc y.
have iuA: A = product2 q b.
  set_extens u; rewrite /A segment_rw /y /glt order_prod2_gle // sb sc;
    rewrite ! product2_rw -/q; bw.
    move=> [[[fgu [du [ua ub]]] [vp2 h]] unv]; ee.
    case h; last by rewrite ordinal_o_lt =>//; exact (elt_of_ordinal oc ua).
    move=> [r1 r2]; move: (wle _ ub) => r3.
    have Wv: w = (V TPb u) by order_tac.
    elim unv; apply fgraph_exten => //; [fprops | bw |].
    rewrite du; move=> x0 x0d; try_lvariant x0d; ue.
  move => [fgu [du [ua ub]]].
  have uc:inc (V TPa u) c by apply sqc.
  ee; first by right; rewrite ordinal_o_lt//; exact (elt_of_ordinal oq ua).
  move=> h; move: (f_equal (V TPa) h); bw => h'.
  by rewrite h' in ua; elim (ordinal_irreflexive oq).
have ss3: substrate pbc = product2 c b.
  by rewrite order_prod2_substrate // sb sc.
have ss2: sub A (substrate pbc) by apply sub_segment.
have sA: sub A (product2 c b) by ue.
have wo2: worder (induced_order pbc A) by apply worder_restriction.
have obq: is_ordinal (ord_prod2 b q) by apply ord_prod2_ordinal => //.
have ->:ord_prod2 b q = ordinal (induced_order pbc A).
  symmetry; apply ordinal_p9 => //.
  rewrite /ord_prod2.
  set r1 := (order_prod2 (ordinal_o b) (ordinal_o q)).
  have wo1: worder r1.
    by rewrite /r1; apply order_prod2_worder; apply ordinal_worder2.
  apply orderIT with r1; last by apply ordinal_p2.
  have or2:order (induced_order pbc A) by fprops.
  have or1:order r1 by fprops.
  suff: r1 = (induced_order pbc A) by move=> ->; apply orderIR.
  rewrite graph_exten; try apply order_is_graph =>//.
  move=> u v.
  rewrite /pbc -[related]/gle iorder_gle5.
  rewrite (order_prod2_gle _ _ orb orq) (order_prod2_gle _ _ orb orc).
  rewrite sb sc sq -iuA; apply iff_eq.
    rewrite /glt/ordinal_o; move=> [up [vp]]; aw; ee.
  move=> [uA [vA [_[_ h]]]]; ee.
  case: h; first (by left); move=> h; right.
  move: uA vA h; rewrite iuA ! product2_rw.
  move=> [_[_ [uq _]]] [_[_ [vq _]]].
  rewrite /glt/ordinal_o;aw; intuition.
set C := induced_order pbc (segment pbc x).
have oraC: order_isomorphic C (ordinal_o a).
  apply orderIS.
  move: om=> [o1 [o2 [injf [sf [tf mof]]]]].
  rewrite /C -rgx.
  have ff: is_function f by fct_tac.
  have sr: sub (range (graph f)) (substrate pbc).
     rewrite tf; fprops; apply f_range_graph =>//.
  have o3: order (induced_order pbc (range (graph f))) by fprops.
  exists (restriction1 f (source f)); red; ee.
          apply restriction1_bijective => //.
      rewrite /restriction1; aw.
      rewrite ordinal_p7// in sf.
    rewrite /restriction1; aw;rewrite image_by_fun_source //; fct_tac.
  rewrite /restriction1; aw.
  move=> u v usf vsf; rewrite restriction1_W // restriction1_W //.
  rewrite /pbc mof // rsub //; apply iff_eq; last by intuition.
  move=> Wuv; ee; apply inc_W_range_graph => //.
rewrite - (ordinal_p3 oa) -(ordinal_p3 odr).
have opbc: order pbc by fprops.
symmetry;apply ord_sum_invariant5 => //.
apply orderIT with C => //.
set fo:= order_sum2 _ _.
have sfo: substrate fo = canonical_du2 A r.
  rewrite /fo order_sum2_substrate; aw;fprops.
have ysp': inc y (product2 c b) by ue.
have xsp': inc x (product2 c b) by ue.
have lexy: gle pbc y x.
  rewrite order_prod2_gle // /y sb sc;bw; ee.
have ltAx: forall t, inc t A -> glt pbc t x.
   move =>t; rewrite /A segment_rw => lttxy; order_tac.
have rprop: forall z, inc z r ->
  inc (variantLc (V TPa x) z) (product2 c b).
  move=> z zB; rewrite product2_rw; bw; ee.
have rprop1: forall z, inc z r -> gle pbc y (variantLc (V TPa x) z).
  move=> z zB; rewrite order_prod2_gle // sb sc; ee; rewrite /y;bw;left; ee.
set g := fun z => Yo (Q z = TPa) (P z) (variantLc (V TPa x) (P z)).
have ssx: sub (segment pbc x) (substrate pbc) by apply sub_segment.
have srC: substrate C = (segment pbc x) by rewrite /C; aw.
have nba: TPb <> TPa by fprops.
have ta: forall z, inc z (substrate fo) -> inc (g z) (substrate C).
  move=> z; rewrite sfo canonical_du2_pr /g; move=> [pz].
  rewrite srC segment_rw.
  case; move => [Pz Qz]; first by Ytac0; apply ltAx => //.
  have [le1 lt1]: glt (ordinal_o b) (P z) (V TPb x).
    by rewrite ordinal_o_lt //; apply srb.
  rewrite Qz (Y_if_not_rw nba) /glt.
  split; first rewrite /pbc (order_prod2_gle _ _ orb orc) sb sc; bw; ee.
  dneg nv; rewrite -nv; bw.
exists (BL g (substrate fo) (substrate C)).
apply total_order_isomorphism => //; aw.
      rewrite /fo;apply order_sum2_totalorder => //.
        apply total_order_sub => //;apply worder_total => //.
      apply worder_total => //.
   rewrite /C; apply order_induced_order => //.
  apply bl_bijective => //.
    move=> u v; rewrite sfo !canonical_du2_pr /g; move=> [pu p3][pv p4].
    case p3; case p4; move=> [p5 p6][p7 p8]; rewrite p6 p8; Ytac0; Ytac0=> aux.
    - apply pair_exten =>//; ue.
    - move: p7; rewrite /A segment_rw => lt1.
      move:(rprop1 _ p5); rewrite -aux => lt2; order_tac.
    - move: p5; rewrite /A segment_rw => lt1.
      move:(rprop1 _ p7); rewrite aux => lt2; order_tac.
   - apply pair_exten => //; [ move: (f_equal (V TPb) aux); bw | ue ].
  move=> v; rewrite srC segment_rw=> hyp.
  case (p_or_not_p (glt pbc v y)) => aux.
    exists (J v TPa); rewrite /g; aw; Ytac0; ee.
    by rewrite sfo canonical_du2_pr; ee; left; aw; ee; rewrite /A segment_rw.
  move: hyp aux; rewrite /glt order_prod2_gle // order_prod2_gle // sb sc.
  move => [[vp [xp aux]] nvx] cvy.
  case aux; last first.
    move=> aux2; elim cvy.
    split; last by rewrite /y;move: aux2 =>[_ vx]; dneg ww; rewrite ww; bw.
    split => //; split => //;rewrite /y; bw; auto.
  move=> [sva leva].
  have vpr: v = variantLc (V TPa x) (V TPb v).
    move: vp; rewrite product2_rw; move=> [a1 [a2 [a3 a4]]].
    apply fgraph_exten => //;[ fprops | bw |].
    rewrite a2; move => z zd; try_lvariant zd.
  have ltva:glt (ordinal_o b) (V TPb v) (V TPb x).
    split => //; clear cvy; dneg ww; rewrite vpr ww.
    symmetry; move:xp; rewrite product2_rw; move=> [a1 [a2 _]].
    apply fgraph_exten => //;[ fprops | bw |].
    rewrite a2; move => z zd; try_lvariant zd.
  exists (J (V TPb v) TPb); rewrite /g; aw; rewrite -vpr; Ytac0.
  rewrite sfo canonical_du2_pr; split; [split; [fprops | right] | trivial].
  aw; ee; rewrite /r -(ordinal_o_lt ob) //.
  move: leva; rewrite /ordinal_o; aw; intuition.
rewrite sfo; rewrite sfo in ta.
have oiA: order (induced_order pbc A) by fprops.
have oor: order (ordinal_o r) by fprops.
move=> u v uc vc; rewrite bl_W // bl_W // /fo /C rsub //.
rewrite order_sum2_gle //.
move=> [_[_ h]]; rewrite -srC; ee.
rewrite /g; case h.
  move=> [h1 [h2 h3]]; Ytac0; Ytac0; apply (iorder_gle1 h3).
case.
  move=> [h1 [h2 h3]]; Ytac0; Ytac0.
  rewrite /pbc order_prod2_gle // sb sc; bw.
  move: h3; rewrite /ordinal_o; aw; move => [h3 [h4 h5]]; ee.
move=> [h1 h2]; Ytac0; Ytac0.
move: uc; rewrite canonical_du2_pr h1; move=> [_].
case; last by move => [_ bad]; elim nba.
rewrite /A segment_rw;move=> [[pa _] _].
move: vc; rewrite canonical_du2_pr.
move=> [_ h0]; case: h0; first by move=> [_ bad]; contradiction.
move=> [h0 _]; move: (rprop1 _ h0) => h4.
order_tac.
Qed.

Lemma ord_division_exists1: forall a b,
  is_ordinal a -> is_ordinal b -> b <> 0c ->
  exists q, exists r, ord_div_pr0 a b q r.
Proof.
move=> a b oa ob bnz.
move: (ord_div_nonzero_b_bis oa ob bnz) => [c [oc p3]].
move: (ord_division_exists oa ob oc p3) => [q [r [p4 _]]].
by exists q; exists r.
Qed.

Lemma limit_ordinal_pr3: forall x,
  limit_ordinal x = (is_ordinal x & x <> 0o &
   (forall y, is_ordinal y -> y +o 1o <> x)).
Proof.
move=> x; apply iff_eq.
  rewrite /limit_ordinal; move=> [h1 [h2 h3]]; ee.
  rewrite /0o/card_zero; move=> h; rewrite h in h2; elim (emptyset_pr h2).
  move=> y yo; rewrite ord_succ_pr // => ysx.
  have yx: inc y x by rewrite - ysx; rewrite /succ_o; fprops.
  move: (h3 _ yx); rewrite ysx; apply (ordinal_irreflexive h1).
move=> [h1 [h2 h3]].
case (limit_ordinal_pr2 h1).
  move=> h4; contradiction.
case => //; move=> [y ys].
have yx: inc y x by rewrite ys; rewrite /succ_o; fprops.
move:(elt_of_ordinal h1 yx) => oy.
elim (h3 _ oy); rewrite ord_succ_pr//.
Qed.

Definition ord_indecomposable z :=
   z <> 0o &
  (forall x y, x <o z -> y <o z -> x +o y <> z).

Lemma indecomp_example: forall x, is_ordinal x -> x <> 0o ->
  ~ (ord_indecomposable (succ_o x)).
Proof.
move=> x or xnz [h1 h2].
have p1: ordinal_lt x (succ_o x) by apply ord_succ_lt.
have p2: ordinal_lt 1o (succ_o x).
  rewrite ord_lt_succ; apply zero_least_ordinal1=>//.
elim (h2 _ _ p1 p2); rewrite ord_succ_pr //.
Qed.

Lemma zero_least_ordinal2: forall x,
  x <o 1o -> x = 0o.
Proof.
move=> x; rewrite ordinal_lt_pr0.
move=> [_[_]]; rewrite /1o /card_one; aw.
Qed.

Lemma indecomp_one: ord_indecomposable 1o.
Proof.
split; first by fprops.
move=> x y xo yo.
rewrite (zero_least_ordinal2 xo) (zero_least_ordinal2 yo).
rewrite (ord_0_plus_unit_l ordinal_0); fprops.
Qed.

Lemma indecomp_omega: ord_indecomposable \omega.
Proof.
split; first by apply ord_omega_non_zero.
move=> x y.
rewrite ! ordinal_lt_pr0 /ord_omega ! omega0_pr2.
move=> [xo [yo xf]] [_ [_ yf]].
have xb: (inc x Bnat) by rewrite inc_Bnat.
have yb: (inc y Bnat) by rewrite inc_Bnat.
rewrite (cardinal_ord_sum2 xb yb) => h.
move: (BS_plus xb yb); rewrite h => h1.
elim (ordinal_decent ordinal_omega h1 h1).
Qed.

Lemma indecomp_omega1: forall x, ord_indecomposable x -> is_ordinal x ->
  x = 1o \/ \omega <=o x.
Proof.
move=> x oix ox.
case (ordinal_le_total_order1 omega0_ordinal ox); first by intuition.
rewrite ordinal_lt_pr0; move => [_ [oo xo]].
case (limit_ordinal_pr2 ox); first by move: oix => [ok _].
case.
  move=> [y yx]; rewrite yx in oix.
  case (equal_or_not y 0o).
    rewrite yx; move=> ->; left; rewrite succ_o_zero //.
  have iyx: inc y x by rewrite yx /succ_o; fprops.
  by move=> ynz; elim (indecomp_example (elt_of_ordinal ox iyx) ynz).
move=> aux; move: (omega0_limit2 aux); rewrite ordinal_le_pr0; intuition.
Qed.

Lemma indecomposable_pr: forall x a b,
  is_ordinal x -> is_ordinal a -> is_ordinal b ->
  ord_indecomposable x -> a +o b = x -> (a = x \/ b = x).
Proof.
move => x a b ox oa ob [_ oix] xs.
move: (ord_sum2_increasing3 oa ob)(ord_sum2_increasing2 oa ob).
rewrite xs => h1 h2.
case (equal_or_not a x); first by intuition.
case (equal_or_not b x); first by intuition.
move => lt1 lt2.
have p1: ordinal_lt a x by split.
have p2: ordinal_lt b x by split.
move: (oix _ _ p1 p2)=> nxs; contradiction.
Qed.

Lemma indecomposable_prop: forall x, is_ordinal x -> x <> 0o ->
  ord_indecomposable x = (forall y, y <o x -> y +o x = x).
Proof.
rewrite / ord_indecomposable; move=> x ox nzx; apply iff_eq.
  move=> [_ oi] y ltyx; move: (ltyx) =>[leyx _].
  move: (ord_sub_pr leyx) => [so se].
  move: (ord_sub_smaller leyx) => ss.
  case (equal_or_not (ord_sub x y) x) => h; first by rewrite h in se.
  have ltxy: ordinal_lt (ord_sub x y) x by split.
  by elim (oi _ _ ltyx ltxy).
move=> h; split=> //; move=> a b lt1 [lt2 ne2].
rewrite - (h _ lt1) => h1; elim ne2.
apply ord_plus_simp_left with a=> //; ord_tac.
Qed.

Lemma indecomposable_prop1: forall x y, ord_indecomposable x ->
  is_ordinal x -> y <o x -> y +o x = x.
Proof.
move=> x y ix ox xy;move: (ix) => [xne _].
by rewrite (indecomposable_prop ox xne) in ix; apply ix.
Qed.

Lemma indecomposable_prod: forall x y, is_ordinal x -> x <> 0o ->
  x <> 1o -> is_ordinal y -> y <> 0o ->
  ord_indecomposable x = ord_indecomposable (y *o x).
Proof.
move=> x y ox xn0 xn1 oy yn0.
apply iff_eq; last first.
  move=> [ha hb]; split => //; move=> a b ax bx.
  move: (ord_mult_compat_lt ax oy yn0) => lt1.
  move: (ord_mult_compat_lt bx oy yn0) => lt2.
  have oa: is_ordinal a by ord_tac.
  have ob: is_ordinal b by ord_tac.
  move: (hb _ _ lt1 lt2); rewrite - order_sum_distributive3 //.
  by move=> h1; dneg h2;rewrite h2.
move=> xi.
move: (ord_prod2_ordinal oy ox) => op.
move: (ord_prod2_nz oy ox yn0 xn0)=> pn0.
rewrite indecomposable_prop //.
move: ordinal_1 => io1.
move=> z ltz.
have oz: is_ordinal z by move: ltz => [[oz _]_].
move: (ord_division_exists oz oy ox ltz)=> [q [r [[oq [or [zv ltrq]]] ltry]]].
symmetry; apply ordinal_le_antisymmetric.
  apply ord_sum2_increasing3=> //.
set t1 := (ord_prod2 y x).
have ot1: is_ordinal t1 by apply ord_prod2_ordinal.
have : ordinal_le z (ord_sum2 (ord_prod2 y q) (ord_prod2 y 1o)).
  rewrite ord_1_mult_unit_r//.
  rewrite zv;apply ord_sum2_increasing1.
    by apply ordinal_le_reflexive; apply ord_prod2_ordinal.
  by move: ltrq => [ok _].
rewrite - order_sum_distributive3 //.
set t2:= (ord_prod2 y (ord_sum2 q 1o)).
move => zt1.
have: ordinal_le (ord_sum2 z t1) (ord_sum2 t2 t1).
   apply ord_sum2_increasing1 => //;ord_tac.
have oq1: is_ordinal (ord_sum2 q 1o) by apply ord_sum2_ordinal.
rewrite /t2 {2 4} /t1 -(order_sum_distributive3 oq1 ox oy).
have ->: (ord_sum2 (ord_sum2 q 1o) x) = x => //.
have spec:ord_sum2 q 1o <> x.
  move: xi=> [_ xi]; apply xi => //.
  split => //; [apply zero_least_ordinal1 => // | intuition ].
rewrite (indecomposable_prop ox xn0) in xi.
apply xi; split=> //; rewrite (ord_succ_pr oq) - ord_succ_lt2 //.
Qed.

Lemma indecomposable_division: forall x y, ord_indecomposable x ->
  is_ordinal x -> is_ordinal y ->
  y <> 0o -> y <o x ->
  exists z, ord_indecomposable z & is_ordinal z & x = y *o z.
Proof.
move=> x y oix ox oy ynz ltyx.
have h1: ordinal_le x (ord_prod2 y x). apply ord_prod2_increasing3 =>//.
case (equal_or_not x (ord_prod2 y x)).
  by exists x; split.
move=> xne.
have xltp: ordinal_lt x (ord_prod2 y x) by split.
move: (ord_division_exists ox oy ox xltp) => [q [r [[oq [or [xeq lt1]]] lt2]]].
symmetry in xeq.
case (indecomposable_pr ox (ord_prod2_ordinal oy oq) or oix xeq) => sx.
  exists q; ee.
  case (equal_or_not q 1o); first by move=> ->; apply indecomp_one.
  move=> qno.
  have xnz: x <> 0o by move: oix => [ok _].
  have qnz: q <> 0o by dneg qz; rewrite -sx qz ord0_prodr //.
  by rewrite (indecomposable_prod oq qnz qno oy ynz) sx.
move: lt1 => [le2 _].
rewrite sx in le2; ord_tac.
Qed.

Lemma indecomposable_prod2: forall a, let b := ord_prod2 a \omega in
  is_ordinal a -> a <> 0o ->
  (ord_indecomposable b & a <o b &
  forall c, ord_indecomposable c -> a <o c -> b <=o c).
Proof.
move=> a b oa anz.
move: ordinal_omega => oo.
move: ord_omega_non_zero => oo0.
have oo1: ord_omega <> 1o.
  move: inc1_Bnat; rewrite -[Bnat]/ord_omega -[card_one]/1o.
  by move=> h1 h2; rewrite h2 in h1; elim (ordinal_decent ordinal_one h1 h1).
rewrite - (indecomposable_prod oo oo0 oo1 oa anz).
split; first by apply indecomp_omega.
split; first by apply (ord_mult_compat_lt1 oa oo anz oo0 oo1).
move=> c oic ac.
have oc: is_ordinal c by move: ac => [[_ [ok _]] _].
move: (indecomposable_division oic oc oa anz ac) => [z [oiz [oz xp]]].
rewrite /b xp.
apply ord_prod2_increasing1; first by apply ordinal_le_reflexive =>//.
case (indecomp_omega1 oiz oz) => //.
move=> z1; move: xp; rewrite z1 ord_1_mult_unit_r//.
by move=> ca; rewrite ca in ac; move: ac => [_ bad].
Qed.

Lemma indecomposable_prod3: forall a, is_ordinal a -> a <> 0o ->
   (succ_o a) *o \omega = a *o \omega.
Proof.
move=>a oa anz.
have: (succ_o a <> 0o).
  have aa: inc a (succ_o a) by rewrite /succ_o; fprops.
  move=> h; rewrite h in aa; elim (emptyset_pr aa).
move: (ord_succ_pr oa) => aux.
rewrite -aux.
move: (ord_sum2_ordinal oa ordinal_one) => oap snz.
move: (indecomposable_prod2 oa anz) (indecomposable_prod2 oap snz).
have ->: card_one = 1o by done.
set (x := ord_prod2 (ord_sum2 a 1o) ord_omega).
set (y:= ord_prod2 a ord_omega).
move => [p1 [p2 p3]] [q1 [q2 q3]].
have ox: is_ordinal x by ord_tac.
have oy: is_ordinal y by ord_tac.
have h1: ordinal_lt a x by rewrite ord_succ_lt2 -aux; move: q2=> [ok _].
move: (p3 _ q1 h1) => yx.
have h2: ordinal_lt (ord_sum2 a 1o) y.
  rewrite (ord_succ_pr oa); split; first by rewrite - ord_succ_lt2//.
  by move=> h; move: (indecomp_example oa anz);rewrite h.
move: (q3 _ p1 h2) => xy; ord_tac.
Qed.

Lemma indecomposable_sup: forall x, is_ordinal x -> x <> 0o ->
  exists y, (ord_indecomposable y & y <=o x &
    forall z, ord_indecomposable z -> z <=o x -> z <=o y).
Proof.
move=> x ox xnz.
set E:= Zo (succ_o x) (fun z => (ord_indecomposable z)).
have ep: forall z, inc z E = (ordinal_le z x & ord_indecomposable z).
  by move=> z; rewrite /E Z_rw (set_ord_le_prop _ ox).
have oE: inc 1o E.
  by rewrite ep;split; [apply zero_least_ordinal1 | apply indecomp_one].
set (F:= fun_image E (fun z => ord_sub x z)).
have neF: nonempty F by exists (ord_sub x 1o); rewrite /F; aw; ex_tac.
have alo: (forall b, inc b F -> ordinal_le b b).
  move=> b; rewrite /F;aw; move=> [z [zE bz]].
  apply ordinal_le_reflexive.
  move: zE; rewrite ep => [[zx] _].
  by move: (ord_sub_pr zx) => [ok _]; rewrite -bz.
move: (wordering_pr wordering_ordinal_le alo) => [p1 [p2 p3]].
rewrite p1 in p3.
move: (p3 _ (@sub_refl F) neF) => [w []]. clear p3.
rewrite substrate_induced_order //; last by rewrite p1.
move=> wF p4.
move: (wF); rewrite /F; aw; move=> [we [weE wep]].
move: weE; rewrite ep ; move=> [p6 p7].
have p5: forall y, inc y E -> ordinal_le (ord_sub x we) (ord_sub x y).
  move=> y yE.
  have sF: inc (ord_sub x y) F by rewrite /F; aw; ex_tac.
  by move: (p4 _ sF); aw; rewrite -wep /gle graph_on_rw1; move=> [_[_]].
clear p4 wF p2 p1 alo neF F oE.
case (equal_or_not x w)=> aux; last first.
  exists we; ee.
  move=> ze zi zx.
  have ize: inc ze E by rewrite ep; ee.
  move: (p5 _ ize) => le1.
  have oz: is_ordinal ze by move: zx => [ok _].
  have owe: is_ordinal we by move: p6 => [ok _].
  move: (ord_sub_pr zx) (ord_sub_pr p6)=> [o1 r1] [o2 r2].
  rewrite wep in le1 o2 r2.
  set (z:= ord_sub x ze) in *.
  case (ordinal_le_total_order1 oz owe) => ltwz; first by auto.
  move: (indecomposable_prop1 zi oz ltwz) => r3.
  move: r2; rewrite {1} r1 -{1} r3 -(order_sum_assoc3 owe oz o1).
  move=> h1.
  move: (ord_plus_simp_left (ord_sum2_ordinal oz o1) o2 owe h1) => hs.
  by elim aux; rewrite r1 hs.
have p8: forall t, ord_indecomposable t -> ordinal_le t x ->
   x = ord_sum2 t x.
  move=> t id tx.
  have te: inc t E by rewrite ep;ee.
  move: (p5 _ te); rewrite wep -aux => le1.
  move:(ord_sub_smaller tx)(ord_sub_pr tx) => le2 [aa bb].
  by move: (ordinal_le_antisymmetric le1 le2) => h3; rewrite {2} h3.
Abort.

Definition ordinal_interval a b := Zo b (fun z => a <=o z).

Lemma ordinal_interval_pr: forall a b z,
  is_ordinal b ->
  inc z (ordinal_interval a b) = (a <=o z & z <o b).
Proof.
move=> a b z ob; rewrite /ordinal_interval Z_rw.
rewrite ordinal_lt_pr0; apply iff_eq; last by intuition.
move=> [zb az]; ee; ord_tac.
Qed.

Lemma ordinal_interval_pr0: forall b z,
  is_ordinal b -> inc z (ordinal_interval 0o b) = z <o b.
Proof.
move=> b z bb;rewrite (ordinal_interval_pr _ _ bb).
apply iff_eq; first by intuition.
by move=> h; ee; apply zero_least_ordinal; ord_tac.
Qed.

Lemma ordinal_interval_pr1: forall b, is_ordinal b ->
  ordinal_interval 0o b = b.
Proof.
move=> b ob; set_extens t; rewrite (ordinal_interval_pr0 _ ob) ordinal_lt_pr0.
  intuition.
move=> h; ee; ord_tac.
Qed.

Lemma ordinal_interval_pr2: forall a b z,
 inc z (ordinal_interval a b) -> is_ordinal z.
Proof.
move=> a b z; rewrite /ordinal_interval Z_rw;move=> [p1 p2]; ord_tac.
Qed.

Lemma ordinal_interval_sup: forall a b, a <o b ->
  \osup (ordinal_interval a b) = \osup b.
Proof.
move=> a b ab.
have ob:is_ordinal b by ord_tac.
have aux: sub (ordinal_interval a b) b.
  move=> t; rewrite (ordinal_interval_pr _ _ ob) ordinal_lt_pr0; intuition.
have osb: ordinal_set b by move=> t tb; apply (elt_of_ordinal ob tb).
apply (ord_sup_pr13 aux osb).
move=> u ub.
have oa: is_ordinal a by ord_tac.
have ou: is_ordinal u by apply osb.
case (ordinal_le_total_order oa ou) => aux1.
  exists u; rewrite (ordinal_interval_pr _ _ ob); ee.
    rewrite ordinal_lt_pr0; ee.
  ord_tac.
exists a;ee; rewrite (ordinal_interval_pr _ _ ob); ee; ord_tac.
Qed.

Lemma ordinal_interval_sup1: forall a b, a <o b -> limit_ordinal b ->
  \osup (ordinal_interval a b) = b.
Proof.
move=> a b ab lb; rewrite ordinal_interval_sup //.
move: ab lb => [[_[ob _]] _].
by rewrite (limit_ordinal_pr1 ob);move => [_ ok].
Qed.

Definition normal_ofs1 f u:=
  (forall x y, u <=o x -> x <o y -> (f x) <o (f y)) &
  (forall X, (forall x, inc x X -> u <=o x) -> nonempty X ->
    \osup (fun_image X f) = f (\osup X)).

Definition normal_ofs2 f u:=
  (forall x y, u <=o x -> x <o y -> (f x) <o (f y)) &
  (forall x, limit_ordinal x -> u <o x ->
    f x = \osup (fun_image (ordinal_interval u x) f)).

Definition normal_ofs f :=
  (forall x y, x <o y -> (f x) <o (f y)) &
  (forall x, limit_ordinal x -> f x = \osup (fun_image x f)).

Lemma normal_ofs1_o: forall f u,
  (forall x y, u <=o x -> x <o y -> (f x) <o (f y))
  -> (forall x, u <=o x -> is_ordinal (f x)).
Proof.
move=> f u pa x ux.
have ox: is_ordinal x by ord_tac.
move: (pa _ _ ux (ord_succ_lt ox)) => pb; ord_tac.
Qed.

Lemma normal_ofs_o: forall f,
  normal_ofs f -> (forall x, is_ordinal x -> is_ordinal (f x)).
Proof.
move=> f [pa _] x ox.
move: (pa _ _ (ord_succ_lt ox)) => pb; ord_tac.
Qed.

Lemma normal_fs_equiv: forall f u,
  normal_ofs1 f u = normal_ofs2 f u.
Proof.
rewrite /normal_ofs1/ normal_ofs2.
move=> f u; apply iff_eq; move=> [p2 p3]; ee.
   move=> x lx ux.
   have bx: is_ordinal x by ord_tac.
   set X := (ordinal_interval u x).
   have p4: (forall x, inc x X -> ordinal_le u x).
     by rewrite /X;move=> y; rewrite (ordinal_interval_pr _ _ bx); intuition.
   have p5: nonempty X.
     have ou: is_ordinal u by ord_tac.
     exists u; rewrite /X ordinal_interval_pr; ee; ord_tac.
   rewrite (p3 _ p4 p5 ) (ordinal_interval_sup1 ux lx) //.
move=> X Xp neX.
move: (normal_ofs1_o p2) => p1.
set Y:= (fun_image X f).
have p4: ordinal_set Y.
  by rewrite /Y; move=> i; aw;move=> [z [zX]] <-; apply p1; apply Xp.
case (inc_or_not (union X) X) => sX.
  have sf: inc (f (union X)) Y by rewrite /Y; aw; ex_tac.
  move: (ord_sup_pr3 p4 sf) => le1.
  have p5: is_ordinal (f (union X)) by apply p1; apply Xp.
  have p6: (forall i, inc i Y -> ordinal_le i (f (union X))).
    move=> i; rewrite /Y; aw; move=> [z [zX]] <-.
    have p7: (forall i, inc i X -> is_ordinal i).
       by move=>j jX; move: (Xp _ jX)=> [_ [ok _]].
    move: (ord_sup_pr3 p7 zX) => h.
    case (equal_or_not z (union X)) => h1; first by rewrite h1; ord_tac.
    have h2: ordinal_lt z (union X) by split.
    by move: (p2 _ _ (Xp _ zX) h2) => [ok _].
  move:(ord_sup_pr4 p4 p5 p6) => le2.
  ord_tac.
have aoX: (forall x, inc x X-> is_ordinal x).
  by move=> x xX; move: (Xp _ xX);move => [_[ok _]].
case (ord_sup_pr9 aoX neX); first by intuition.
move=> ls.
have [x [xX [leux neux]]]: exists x, inc x X & ordinal_lt u x.
  apply exists_proof; move=> h.
  move: neX => [y yX]; case (equal_or_not u y); last first.
    by move=> yu; elim (h y); ee; split => //; apply (Xp _ yX).
  move=> uy; rewrite -uy in yX.
  case (equal_or_not X (singleton u)) => Xu.
    rewrite {1} Xu union_singleton in sX; contradiction.
  have [z [zX zu]]: exists z, inc z X & z <> u.
    apply exists_proof; move=> h1; elim Xu; set_extens t; aw;last by move=> ->.
    move=> tX; ex_middle h2; elim (h1 t); ee.
  elim (h z); ee; split; [ apply (Xp _ zX) | intuition ].
move: (ord_sup_pr3 aoX xX) => le1.
have ltus: ordinal_lt u (union X).
  split; [ord_tac | dneg uns; rewrite -uns in le1;ord_tac ].
rewrite (p3 _ ls ltus).
move: (le1) => [_ [oos _]].
have sXoi: sub X (ordinal_interval u (union X)).
  move=> t tX; rewrite ordinal_interval_pr //.
  by split; [ apply Xp | apply ord_sup_pr8].
set Z:= (fun_image (ordinal_interval u (union X)) f).
have sFxoi: sub (fun_image X f) Z.
  rewrite /Z;move => t; aw; move=> [z [zX fz]]; exists z; ee.
have Zp: (forall z, inc z Z -> is_ordinal z).
  move=> z; rewrite /Z; aw; move=> [v [vi]] <-; apply p1.
  move: vi; rewrite ordinal_interval_pr //; intuition.
move: (ord_sum_pr10 sFxoi Zp) => h1.
apply ordinal_le_antisymmetric => //.
apply ord_sup_pr4 => //.
  by apply ord_sup_pr1; move=> i ifi; apply Zp; apply sFxoi.
have aux1: is_ordinal (union X) by apply ord_sup_pr1.
move=> i; rewrite /Z; aw; move=> [z]; rewrite ordinal_interval_pr//.
move=> [[uz zsX]] <-.
have [t [tX zt]]: exists t, inc t X & ordinal_le z t.
  apply exists_proof; move=> h.
  have oz: is_ordinal z by move: uz => [_ [ok _]].
  have h2: forall x, inc x X -> ordinal_le x z.
    move=> v vX.
    case (ordinal_le_total_order oz (aoX _ vX)) => // h3.
    elim (h v); ee.
  move: (ord_sup_pr4 aoX oz h2) => h3.
  move:zsX => [h4 h5].
  rewrite (ordinal_le_antisymmetric h3 h4) in h5.
  by elim h5.
have aux: ordinal_le (f t) (union Y).
  rewrite /Y; apply ord_sup_pr3 => //; aw; ex_tac.
case (equal_or_not z t) => ezt; first by ue.
have lzt: ordinal_lt z t by split.
move: (p2 _ _ uz lzt)=> [aux2 _]; ord_tac.
Qed.

Lemma normal_fs_equiv1: forall f,
  normal_ofs1 f 0o = normal_ofs f.
Proof.
move=> f;rewrite normal_fs_equiv; rewrite /normal_ofs2 /normal_ofs.
apply iff_eq; move=> [h2 h3]; eee.
- move=> x y xy; apply h2=> //; apply zero_least_ordinal.
  by move: xy=> [[ox _] _].
- move=> x xl.
  have ox: is_ordinal x by move: xl =>[ok _].
  rewrite - {2} (ordinal_interval_pr1 ox).
  apply h3 => //; rewrite ordinal_lt_pr0.
  red in xl; ee; apply ordinal_zero.
- by move=> x y r1 r2; apply h2.
- move => x lx wnz.
  have ox: is_ordinal x by move: lx =>[ok _].
  by rewrite (ordinal_interval_pr1 ox); apply h3.
Qed.

Lemma normal_fs_equiv2: forall f a,
  is_ordinal a -> normal_ofs f-> normal_ofs1 f a.
Proof.
move=> f a oa;rewrite - normal_fs_equiv1 /normal_ofs1.
move=> [p2 p3]; ee.
   move=> x y xp yp; apply p2 =>//; apply zero_least_ordinal; ord_tac.
move=> X xp xX; rewrite p3 //.
move=> t tx; move: (xp _ tx)=> h; apply zero_least_ordinal; ord_tac.
Qed.

Lemma ord_sum2_succ: forall a b, is_ordinal a -> is_ordinal b ->
   succ_o (a +o b) = a +o (succ_o b).
Proof.
move=> a b oa ob.
rewrite -(ord_succ_pr ob) (order_sum_assoc3 oa ob ordinal_one) ord_succ_pr //.
apply (ord_sum2_ordinal oa ob).
Qed.

Lemma ord_plus_normal: forall a, is_ordinal a ->
 normal_ofs (fun u => a +o u).
Proof.
move=> a aB; red; ee.
  by move=> x y xy; apply ord_plus_compat_lt.
move=> x olx.
have ox: is_ordinal x by move: olx => [ok _].
move: (ord_sum2_ordinal aB ox)=> oax.
set ss:= fun_image x (fun u => a +o u).
have os: ordinal_set ss.
  rewrite /ss;move =>t;aw; move=> [z [zx]] <-.
  apply ord_sum2_ordinal => //; ord_tac.
have p1: (union ss) <=o (a +o x).
  apply ord_sup_pr4 => //.
  rewrite /ss;move=> i; aw; move=> [z [zx]] <-; apply ord_sum2_increasing1.
    ord_tac.
  by move: zx;rewrite (set_ord_lt_prop _ ox); move=> [ok _].
move:(ord_sub_pr p1) => [p2 p3].
set d := ((a +o x) -o (union ss)) in p2 p3.
have ass: inc a ss.
  rewrite /ss; aw; exists 0o; ee; first by move: olx => [_ [ok _]].
  rewrite ord_0_plus_unit_r //.
move:(ord_sub_pr (ord_sup_pr3 os ass)) => [p4 p5].
set e := ((union ss) -o a) in p4 p5.
rewrite p5 in p3; rewrite - order_sum_assoc3 // in p3.
move: (ord_plus_simp_left ox (ord_sum2_ordinal p4 p2) aB p3) => xed.
case (equal_or_not d 0o).
  move=> dz; rewrite p5 p3 dz (ord_0_plus_unit_r p4); apply refl_equal.
move=> dnz.
have lex:(e <o x).
  rewrite xed; split; first by apply (ord_sum2_increasing2 p4 p2).
  dneg eed; apply (ordinal_a_ne_ab p4 p2 eed).
have lesx: inc (succ_o e) x.
  by move: olx => [_[_ h]]; apply h; rewrite (set_ord_lt_prop _ ox).
have le3: inc (ord_sum2 a (succ_o e)) ss by rewrite /ss; aw; ex_tac.
move: (ord_sup_pr3 os le3).
rewrite -(ord_sum2_succ aB p4) -p5 => h1.
move: (ord_sup_pr1 os)=> oos.
move: (ord_succ_lt oos) => h2.
ord_tac.
Qed.

Lemma ord_prod_normal: forall a, is_ordinal a ->
 a <> 0o -> normal_ofs (fun u => a *o u).
Proof.
move=> a aB anz; red; ee.
  by move=> x y xy; apply ord_mult_compat_lt.
move=> x olx.
have ox: is_ordinal x by move: olx => [ok _].
move: (ord_prod2_ordinal aB ox)=> oax.
set ss:= fun_image x (fun u => ord_prod2 a u).
have os: ordinal_set ss.
  rewrite /ss;move =>t;aw; move=> [z [zx]] <-.
  apply ord_prod2_ordinal => //; ord_tac.
have p1: (union ss) <=o (a *o x).
  apply ord_sup_pr4 => //.
  rewrite /ss;move=> i; aw; move=> [z [zx]] <-; apply ord_prod2_increasing1.
  apply ordinal_le_reflexive => //.
  by move: zx;rewrite (set_ord_lt_prop _ ox); move=> [ok _].
symmetry;ex_middle neq.
have lt1: (union ss) <o (a *o x) by split.
move: (ord_sup_pr1 os)=> oos.
move: (ord_division_exists oos aB ox lt1) => [q [r [[oq [or [av ltrb]]] ltqc]]].
move: (ord_prod2_ordinal aB oq)=> aqo.
move: (ord_plus_compat_lt ltrb aqo). rewrite -av.
rewrite -{2} (ord_1_mult_unit_r aB).
rewrite -(order_sum_distributive3 oq ordinal_one aB).
rewrite (ord_succ_pr oq).
have lesx: inc (succ_o q) x.
  by move: olx => [_[_ h]]; apply h; rewrite (set_ord_lt_prop _ ox).
have le3: inc (ord_prod2 a (succ_o q)) ss by rewrite /ss; aw; ex_tac.
move: (ord_sup_pr3 os le3)=> h1 [h2 h3]; elim h3; ord_tac.
Qed.

Lemma ordinal_worder4: forall x (p: Set -> Prop),
 is_ordinal x -> p x ->
 let y := least_ordinal p x in
   is_ordinal y & p y & (forall z, is_ordinal z -> p z -> y <=o z ).
Proof.
move=> x p ox px y; move: (ordinal_worder1 ox px) => [p1 [p2 p3]].
ee; move=> t ot pt;move: (p3 _ ot pt);rewrite ordinal_le_pr0; move=> zt; ee.
Qed.

Lemma ordinal_worder3: forall x (p: Set -> Prop),
 is_ordinal x -> ~ (p x) ->
 let y := least_ordinal (fun z => (~ p z)) x in
   is_ordinal y & ~(p y) & (forall z, z <o y -> p z).
Proof.
move=> x p ox px y.
move: (ordinal_worder4 (p:= (fun z : Set => ~ p z)) ox px) => [p1 [p2 p3]].
ee; move=> z zy.
have oz: is_ordinal z by ord_tac.
ex_middle npz; move: (p3 _ oz npz) => lt; ord_tac.
Qed.

Lemma ordinal_worder5: forall x (p: Set -> Prop),
 1o <=o x -> ~(p x) ->
 let y := least_ordinal (fun z => (~ (1o <=o z -> p z))) x in
   is_ordinal y & (1o <=o y) & ~(p y) &
    (forall z, inc z (ordinal_interval 1o y) -> p z).
Proof.
move=> x p ox px.
set (q := (fun z : Set =>(1o <=o z -> p z))).
have orx: is_ordinal x by ord_tac.
case (p_or_not_p (q x)); first by rewrite /q; intuition.
move=> nq.
move: (ordinal_worder3 orx nq) => /=.
rewrite /q.
set (y := (least_ordinal (fun z : Set => ~ (1o <=o z -> p z)) x)).
move=> [y1 [y2 y3]]; ee.
  ex_middle h; elim y2; intuition.
move=> z; rewrite ordinal_interval_pr //; move=> [z1 z2].
apply ((y3 _ z2) z1).
Qed.

Definition ord_induction_axioms w g u:=
  (forall x, u <=o x -> x <=o (w x)) &
  (forall x y, u <=o x -> u <=o y -> ordinal_lt x (g x y)).

Definition ord_induction_prop w0 w1 g u f:=
  (forall x, u <=o x -> f x 0o = w0 x) &
  (forall x, u <=o x -> f x 1o = w1 x) &
  (forall x y, u <=o x -> ordinal_lt 1o y ->
    f x y = union (fun_image (ordinal_interval 1o y)
                         (fun z => g (f x z) x))).

Lemma ord_induction_unique: forall w0 w1 g u f f',
   ord_induction_prop w0 w1 g u f -> ord_induction_prop w0 w1 g u f' ->
   forall x y, u <=o x -> is_ordinal y -> f x y = f' x y.
Proof.
move=> w0 w1 g u f f' [h2 [h3 h4]] [h2' [h3' h4']] x y0 ux oy0.
ex_middle bad0.
set p:= fun y => f x y = f' x y.
have py0: ~ (p y0) by [].
move: (ordinal_worder3 oy0 py0) => [oy [py lpy]].
set (y :=least_ordinal (fun z : Set => ~ p z) y0) in *.
elim py; rewrite /p.
case (equal_or_not 0o y) => ey0; first by rewrite -ey0 h2// h2' //.
case (equal_or_not 1o y) => ey1; first by rewrite -ey1 h3// h3' //.
have lty1: ordinal_lt 1o y.
  split=>//; apply zero_least_ordinal1 => //; intuition.
rewrite h4 // h4'//; apply f_equal.
suff rec: forall z, inc z (ordinal_interval 1o y) -> f x z = f' x z.
 set_extens t;aw; move=> [z [zi]] <-; exists z; ee; rewrite (rec _ zi) //.
move=> z; rewrite ordinal_interval_pr//; move=> [z1 zy].
by apply lpy.
Qed.

Definition ord_induction_aux (w0 w1: Set-> Set) g a b :=
  transfinite_defined (ordinal_o b)
  (fun f => Yo (source f = 0o) (w0 a)
    (Yo (source f = 1o) (w1 a)
      (union (fun_image (ordinal_interval 1o (source f))
        (fun z => g (W z f) a))))).

Definition ord_induction_defined w0 w1 g :=
  fun x y => W y (ord_induction_aux w0 w1 g x (succ_o y)).

Lemma ord_induction_p0: forall w0 w1 g a b, is_ordinal b ->
  let f := (ord_induction_aux w0 w1 g a b) in
     (is_function f & source f = b &
       (inc 0o b -> W 0o f = w0 a) &
       (inc 1o b -> W 1o f = w1 a) &
       (forall x, inc x b -> 1o <o x ->
         W x f = (union (fun_image (ordinal_interval 1o x)
           (fun z => g (W z f) a))))).
Proof.
move=> w0 w1 g a b bb f.
set p := (fun f => (Yo (source f = 0o) (w0 a)
    (Yo (source f = 1o) (w1 a)
      (union (fun_image (ordinal_interval 1o (source f))
        (fun z => g (W z f) a)))))).
move: (transfinite_defined_pr p (ordinal_worder2 bb)).
rewrite /transfinite_def (ordinal_p7 bb) //.
have sh: forall c, inc c b -> source
  (restriction_to_segment (ordinal_o b) c
    (transfinite_defined (ordinal_o b) p)) = c.
  move=> c cb; rewrite /restriction_to_segment /restriction1; aw.
  apply ordinal_segment => //.
move=> [[h1 _] [h2 h3]]; ee.
- move=> zb;rewrite (h3 _ zb).
  set h := restriction_to_segment _ _ _.
  by rewrite /p Y_if_rw //; apply sh.
- move=> zb; rewrite (h3 _ zb); move: (sh _ zb) => sh1.
  have onz: 1o <> 0o by fprops.
  by rewrite /p sh1; Ytac0; Ytac0.
- move => x xb; rewrite (h3 _ xb); move: (sh _ xb) => sh1.
  move=> [l1 l2].
  have l3: x <> 1o by intuition.
  have l4: x <> 0o by apply zero_least_ordinal5.
  rewrite {1} /p sh1; Ytac0; Ytac0;apply f_equal.
  have ox: is_ordinal x by ord_tac.
  have aux: forall z, inc z (ordinal_interval 1o x) ->
     W z f = W z (restriction_to_segment (ordinal_o b) x
                (transfinite_defined (ordinal_o b) p)).
    move=> z; rewrite ordinal_interval_pr//; move=> [l5 l6].
    have zx: inc z x by move: l6; rewrite ordinal_lt_pr0; intuition.
    have lt1: glt (ordinal_o b) z x.
      rewrite ordinal_o_lt //; apply (ordinal_transitive bb xb zx).
    rewrite rts_W //; red; ee.
        apply ordinal_worder2 => //.
      rewrite ordinal_p7 //.
    rewrite h2 - {2} (ordinal_p7 bb); apply sub_segment.
  set_extens t; aw; move=> [z [z1 z2]]; ex_tac; rewrite -z2 (aux _ z1) //.
Qed.

Lemma ord_induction_p1: forall w0 w1 g x,
  ord_induction_defined w0 w1 g x 0o = w0 x.
Proof.
move=> w0 w1 g x;set b:= succ_o 0o.
have zb: (inc 0o b) by rewrite /b /succ_o; fprops.
have ob: is_ordinal b by apply ordinal_succ; apply ordinal_zero.
by move: (ord_induction_p0 w0 w1 g x ob) => [_ [ _ [h1 _]]]; apply h1.
Qed.

Lemma ord_induction_p2: forall w0 w1 g x,
  ord_induction_defined w0 w1 g x 1o = w1 x.
Proof.
move=> w0 w1 g x;set b:= succ_o 1o.
have zb: (inc 1o b) by rewrite /b /succ_o; fprops.
have ob: is_ordinal b by apply ordinal_succ; apply ordinal_one.
by move: (ord_induction_p0 w0 w1 g x ob) => [_ [_ [ _ [h1 _]]]]; apply h1.
Qed.

Lemma ord_induction_p3: forall w0 w1 g a b1 b2 x,
  is_ordinal b1 -> is_ordinal b2 ->
  inc x b1 -> inc x b2 -> is_ordinal x ->
  let f1 := (ord_induction_aux w0 w1 g a b1) in
  let f2 := (ord_induction_aux w0 w1 g a b2) in
     W x f1 = W x f2.
Proof.
move=> w0 w1 g a b1 b2 x ob1 ob2 xb1 xb2 x1 f1 f2.
set p:= fun z => inc z b1 -> inc z b2 -> W z f1 = W z f2.
case (p_or_not_p (p x)) ; first by apply.
move => px; move: (ordinal_worder3 x1 px) => [oz [zp1 zp2]].
set (t:= (least_ordinal (fun z0 : Set => ~ p z0) x)) in *.
elim zp1; move=> tb1 tb2.
move: (ord_induction_p0 w0 w1 g a ob1) => [_ [_ [h0 [h1 hg]]]].
move: (ord_induction_p0 w0 w1 g a ob2) => [_ [_ [h0' [h1' hg']]]].
case (equal_or_not 0o t) => ez0.
  rewrite -ez0 /f1 /f2 h0 ?h0'//;ue.
case (equal_or_not 1o t) => ez1.
  rewrite -ez1 /f1 /f2 h1 ?h1'//; ue.
have lty1: ordinal_lt 1o t.
  split=>//; apply zero_least_ordinal1 => //; intuition.
rewrite (hg _ tb1 lty1) (hg' _ tb2 lty1).
apply ord_sup_pr12.
move=> z; rewrite ordinal_interval_pr//; move=> [zt ltwz].
have zb1: inc z b1.
  move: tb1; rewrite !(set_ord_lt_prop _ ob1); move=> [aux _]; ord_tac.
have zb2: inc z b2.
  move: tb2; rewrite !(set_ord_lt_prop _ ob2); move=> [aux _]; ord_tac.
rewrite ((zp2 z ltwz) zb1 zb2) //.
Qed.

Lemma ord_induction_exists: forall w0 w1 g u,
   ord_induction_prop w0 w1 g u (ord_induction_defined w0 w1 g).
Proof.
move=> w0 w1 g u; split; first by move=> x; rewrite ord_induction_p1 //.
split; first by move=> x; rewrite ord_induction_p2 //.
move=> x y ux y1.
rewrite /ord_induction_defined.
have oy: is_ordinal y by ord_tac.
have ob: is_ordinal (succ_o y) by fprops.
have iyb: inc y (succ_o y) by rewrite /succ_o; fprops.
move: (ord_induction_p0 w0 w1 g x ob) => [_ [_ [h0 [h1 hg]]]].
rewrite (hg _ iyb y1).
apply f_equal.
suff A: forall t, inc t (ordinal_interval 1o y) ->
    W t (ord_induction_aux w0 w1 g x (succ_o y)) =
    W t (ord_induction_aux w0 w1 g x (succ_o t)).
  set_extens t; aw; move=> [w [z1 z2]]; ex_tac; rewrite -z2 (A _ z1) //.
move=> t; rewrite ordinal_interval_pr // ordinal_lt_pr0; move=> [_[_[_ ty]]].
have bt: is_ordinal t by ord_tac.
move: (ordinal_transitive ob iyb ty) => tb.
apply ord_induction_p3 => //; fprops;rewrite /succ_o;fprops.
Qed.

Lemma ord_induction_p4: forall w0 w1 g u x y,
  ord_induction_axioms w1 g u ->
  u <=o x -> 1o <=o y ->
  x <=o (ord_induction_defined w0 w1 g x y).
Proof.
move=> w0 w1 g u x y0 oa ux0 loy0.
set f :=ord_induction_defined w0 w1 g x.
ex_middle npy0.
move: (ordinal_worder5 loy0 npy0 (p:= fun z => ordinal_le x (f z))) => /=.
set z := least_ordinal _ _; move=> [oz [z1 [npz lpy]]]; elim npz.
move: (oa)=> [oa1 oa3].
move: (oa1 _ ux0) => le1.
case (equal_or_not 1o z)=> x2.
  rewrite -x2 /f ord_induction_p2 => //.
have x3: ordinal_lt 1o z by split.
move: (ord_induction_exists w0 w1 g u); move=> [_ [r0 r00]].
have r1: f 1o = w1 x by rewrite /f r0.
rewrite /f r00 // -/f; clear r0 r00.
set T:= fun_image _ _.
have oT: ordinal_set T.
  move=> t; rewrite /T; aw; move=> [w [wc]] <-.
  move: (lpy _ wc) => le2.
  have aux3: ordinal_le u (f w) by ord_tac.
  move: (oa3 _ _ aux3 ux0)=> [le3 _]; ord_tac.
have sT: inc (g (f 1o) x) T.
  rewrite /T; aw; exists 1o; rewrite ordinal_interval_pr; ee.
   move: ordinal_one => aux;ord_tac.
move: (ord_sup_pr3 oT sT); rewrite r1=> r3.
have lr2: ordinal_le u (w1 x) by ord_tac.
move: (oa3 _ _ lr2 ux0) => [le2 _].
apply (ordinal_le_transitive (ordinal_le_transitive le1 le2) r3).
Qed.

Lemma ord_induction_p41: forall w0 w1 g u x y,
  ord_induction_axioms w1 g u ->
  u <=o x -> 1o <=o y ->
  u <=o (ord_induction_defined w0 w1 g x y).
Proof.
move=> w0 w1 g u x y oa ux y1; move: (ord_induction_p4 w0 oa ux y1).
move=> aux; ord_tac.
Qed.

Lemma ord_induction_p5: forall w0 w1 g u x y,
  ord_induction_axioms w1 g u ->
  u <=o x -> 1o <=o y ->
  is_ordinal (ord_induction_defined w0 w1 g x y).
Proof.
move=> w0 w1 g u x y oa ux y1; move: (ord_induction_p4 w0 oa ux y1) => h.
ord_tac.
Qed.

Lemma ord_induction_p6: forall w0 w1 g u x y,
  ord_induction_axioms w1 g u ->
  u <=o x -> 1o <=o y ->
  is_ordinal (g (ord_induction_defined w0 w1 g x y) x).
Proof.
move=> w0 w1 g u x y oa ux y1; move: (ord_induction_p41 w0 oa ux y1).
set f := ord_induction_defined w0 w1 g x.
move: oa=> [oa1 oa3].
move=> h1; move: (oa3 _ _ h1 ux)=> h2; ord_tac.
Qed.

Lemma ord_induction_p7: forall w0 w1 g u x y y',
  ord_induction_axioms w1 g u ->
  u <=o x -> 1o <=o y ->
  y <o y' ->
  let f := ord_induction_defined w0 w1 g x in
  (g (f y) x) <=o (f y').
move=> w0 w1 g u x y z oa ux y1 yz f.
move: (ord_induction_exists w0 w1 g u); move=> [_ [_ r00]].
rewrite {2}/f r00 // -/f; last by ord_tac.
have oz: is_ordinal z by ord_tac.
set T:= fun_image _ _.
have oT: ordinal_set T.
  move=> t; rewrite /T; aw; move=> [w [wc]] <-.
  move: wc; rewrite (ordinal_interval_pr _ _ oz); move=> [wp1 wp2].
  apply (ord_induction_p6 oa ux wp1).
have fyt: (inc (g (f y) x) T).
  rewrite /T; aw; exists y; ee.
  rewrite ordinal_interval_pr //.
apply (ord_sup_pr3 oT fyt).
Qed.

Lemma ord_induction_p8: forall w0 w1 g u x y y',
  ord_induction_axioms w1 g u ->
  u <=o x -> 1o <=o y ->
  y <o y' ->
  let f := ord_induction_defined w0 w1 g x in
  (f y) <o (f y').
Proof.
move=> w0 w1 g u x y z oa ux y1 yz f.
move: (ord_induction_p7 w0 oa ux y1 yz); simpl; rewrite -/f => le1.
move: (oa)=> [oa1 oa3].
move: (ord_induction_p41 w0 oa ux y1) => le2.
move: (oa3 _ _ le2 ux) => le3; ord_tac.
Qed.

Lemma ord_induction_p9: forall w0 w1 g u x y,
  ord_induction_axioms w1 g u ->
  u <=o x -> 1o <=o x -> 1o <=o y ->
  y <=o (ord_induction_defined w0 w1 g x y).
Proof.
move=> w0 w1 g u x y oa ux x1 y1.
set f :=ord_induction_defined w0 w1 g x.
set p:= fun z => ordinal_le 1o z -> ordinal_le z (f z).
case (p_or_not_p (p y)); [by apply | move => py].
have oy: is_ordinal y by ord_tac.
move: (ordinal_worder3 oy py) => [oz [pt lpy]].
set (t := least_ordinal (fun z0 : Set => ~ p z0) y) in *.
elim pt => z1.
move: (ord_induction_p4 w0 oa ux z1); rewrite -/f =>h.
move: (ordinal_le_transitive x1 h) => f1.
have orf: is_ordinal (f t) by ord_tac.
case (ordinal_le_total_order1 oz orf)=> // p3z.
move: ((lpy _ p3z) f1).
move: (ord_induction_p8 w0 oa ux f1 p3z) => /=; rewrite -/f.
move=> h1 h2; ord_tac.
Qed.

Lemma ord_induction_p10: forall w0 w1 g u x,
  ord_induction_axioms w1 g u -> ordinal_le u x ->
  normal_ofs1 (ord_induction_defined w0 w1 g x) 1o.
Proof.
move=> w0 w1 g u x oa ux.
rewrite normal_fs_equiv.
set f:= ord_induction_defined w0 w1 g x.
have aux: forall y, 1o <=o y -> is_ordinal (f y).
  move=> y oy; apply (ord_induction_p5 oa ux oy).
split; first by move=> y y' y1; apply (ord_induction_p8 w0 oa ux y1).
move=> y ly oy1.
set T:= fun_image _ _.
have oy: is_ordinal y by ord_tac.
have oT: ordinal_set T.
  move=> v ;rewrite /T;aw; move=>[z [zy]] <-.
  move: zy; rewrite ordinal_interval_pr//; move=> [oz zy]; apply aux =>//.
move: (oy1) => [oy2 _].
have le1: (union T) <=o (f y).
  apply ord_sup_pr4 => //; first by apply aux.
  move=> i; rewrite /T; aw; move=>[z]; rewrite ordinal_interval_pr//.
  move=> [[oz1 oz2] zy]; move: (ord_induction_p8 w0 oa ux oz1 oz2)=> [h _]; ue.
move: (ord_induction_exists w0 w1 g u); move=> [_ [_ oag]].
suff le2: (f y) <=o (union T) by ord_tac.
rewrite /f (oag _ _ ux oy1); clear oag.
apply ord_sup_pr4.
    move=> t; aw; move=> [z]; rewrite ordinal_interval_pr//.
    move=> [[z1 z2]] <-; apply (ord_induction_p6 oa ux z1).
  apply ord_sup_pr1 => //.
move=> i; aw; move=> [z]; rewrite ordinal_interval_pr//; move=> [[oz zy]].
rewrite -/f; move => <-.
have orz: is_ordinal z by ord_tac.
move: (ord_succ_lt orz) => orsz.
move: (ord_induction_p7 w0 oa ux oz orsz); simpl; rewrite -/f => le2.
suff ft: inc (f (succ_o z)) T by move: (ord_sup_pr3 oT ft)=> le3; ord_tac.
rewrite /T; aw; exists (succ_o z); rewrite ordinal_interval_pr; ee.
   move: orsz=> [le3 _]; ord_tac.
move: zy; rewrite !ordinal_lt_pr0; move=> [_[_ izy]]; ee.
move:ly =>[_ [_]]; by apply.
Qed.

Lemma ord_induction_p11: forall w0 w1 g u x b y y',
  ord_induction_axioms w1 g u -> u <=o x ->
  1o <=o y -> 1o <=o y' ->
  let f := ord_induction_defined w0 w1 g x in
    (f y) <=o b -> b <o (f (succ_o y)) ->
    (f y') <=o b -> b <o (f (succ_o y')) ->
    y = y'.
Proof.
move=> w0 w1 g u x b y y' oa ux y1 y'1 f le1 le2 le3 le4.
have oy: is_ordinal y by ord_tac.
have oy': is_ordinal y' by ord_tac.
have lt1: (f y) <o (f (succ_o y')) by ord_tac.
have lt2: (f y') <o (f (succ_o y)) by ord_tac.
ex_middle yy'.
case (ordinal_le_total_order1 oy oy').
   move=> h; have: y <o y' by split.
   rewrite ord_succ_lt2 // => h2.
   case (equal_or_not (succ_o y) y').
     by move=> h3; move: lt2=> [_]; rewrite h3.
   move=> h3; have h4: (succ_o y) <o y' by split.
   have h5: 1o <=o (succ_o y).
      move: (ord_succ_lt oy) => [h6 _]; ord_tac.
   move: (ord_induction_p8 w0 oa ux h5 h4); simpl.
   rewrite -/f; move => [h1 _]; ord_tac.
rewrite ord_succ_lt2 // => h2.
case (equal_or_not (succ_o y') y).
  by move=> h3; move: lt1=> [_]; rewrite h3.
move=> h3; have h4: (succ_o y') <o y by split.
have h5: 1o <=o (succ_o y').
 move: (ord_succ_lt oy') => [h6 _]; ord_tac.
move: (ord_induction_p8 w0 oa ux h5 h4); simpl.
rewrite -/f; move => [h1 _]; ord_tac.
Qed.

Lemma ord_induction_p12: forall w0 w1 g u x b,
  ord_induction_axioms w1 g u -> ordinal_le u x ->
  (w1 x) <=o b -> 1o <=o x ->
  let f := ord_induction_defined w0 w1 g x in
    exists y,
     1o <=o y & y <=o b & (f y) <=o b & b <o (f (succ_o y)).
Proof.
move=> w0 w1 g u x b oa ux w1b w2b f.
have b1:ordinal_le 1o b.
  move: (oa) => [oa1 _]; move: (oa1 _ ux) => le1.
  apply (ordinal_le_transitive (ordinal_le_transitive w2b le1) w1b).
have ob: is_ordinal b by ord_tac.
have pb: ~ ((f (succ_o b)) <=o b).
  move => l1.
  move: (ord_succ_lt ob)=> lt1.
  have [le2 _]:1o <o (succ_o b) by ord_tac.
  move: (ord_induction_p9 w0 oa ux w2b le2).
  rewrite - ord_succ_lt2 -/f; move=> l2; ord_tac.
move: (ordinal_worder5 b1 pb (p:=fun y => ordinal_le (f (succ_o y)) b)) => /=.
set t := least_ordinal _ _; move=> [ot [t1 [pt lpy]]].
have letb: ordinal_le t b.
  case (ordinal_le_total_order1 ot ob) => // ltbt.
  have bi:(inc b (ordinal_interval 1o t))
      by rewrite ordinal_interval_pr //; ee.
  move: (lpy _ bi) => pb1; contradiction.
have t2: b <o (f (succ_o t)).
  have t0: 1o <=o (succ_o t).
    apply zero_least_ordinal1; first by apply ordinal_succ.
    rewrite /succ_o /0o/card_zero; move=> bad.
    have te: inc t emptyset by rewrite -bad; fprops.
    elim (emptyset_pr te).
  have orf: is_ordinal (f (succ_o t)).
    rewrite /f; apply (ord_induction_p5 oa ux t0).
  case (ordinal_le_total_order1 orf ob) => //.
exists t;ee.
case (equal_or_not 1o t) => to.
  rewrite -to /f (ord_induction_p2 w0 w1 g x) => //.
have lt1: ordinal_lt 1o t by split.
case (limit_ordinal_pr2 ot); first by move:(zero_least_ordinal5 t1); intuition.
case.
  move=> [y ts]. rewrite ts.
  have oy: is_ordinal y
     by apply (elt_of_ordinal ot); rewrite ts /succ_o; fprops.
  have yi: inc y (ordinal_interval 1o t).
    rewrite ordinal_interval_pr // ts;ee; last by apply (ord_succ_lt oy).
    apply zero_least_ordinal1 => //; move=> yz.
    elim to; rewrite ts yz; symmetry;apply succ_o_zero.
  apply (lpy _ yi).
move=> lt.
move: (ord_induction_p10 w0 oa ux); rewrite normal_fs_equiv; move=> [_ nn].
move: (nn _ lt lt1); rewrite -/f; move=> ->.
set T:= fun_image _ _.
have oT: ordinal_set T.
  move=> v ;rewrite /T;aw; move=>[z [zy]] <-.
  move: zy; rewrite ordinal_interval_pr//; move=> [oz1 zy1].
  apply (ord_induction_p5 oa ux oz1).
apply ord_sup_pr4 => //.
move=> i; rewrite /T; aw; move=>[z [zi]] <-.
move: (lpy _ zi) => le1.
move: zi;rewrite (ordinal_interval_pr _ _ ot); move=> [oz1 oz2].
have bz: is_ordinal z by ord_tac.
move: (ord_induction_p8 w0 oa ux oz1 (ord_succ_lt bz)); simpl; rewrite -/f.
move => [le3 _]; ord_tac.
Qed.

Lemma ord_induction_p13: forall a b,
  is_ordinal a -> is_ordinal b ->
  ord_induction_defined id succ_o (fun u v:Set => succ_o u) a b
  = a +o b.
Proof.
move=> a b.
set g := (fun a b:Set => succ_o a).
move=> oa ob.
have ooa: ordinal_le 0o a by apply zero_least_ordinal.
have oax: ord_induction_axioms succ_o g 0o.
  split.
    move=> x xz.
    have ox: is_ordinal x by ord_tac.
    by move: (ord_succ_lt ox) => [ok _].
  move=> x y x0 y0; rewrite /g; apply ord_succ_lt; ord_tac.
move: (ord_induction_exists id succ_o g 0o) => p1.
suff p2: (ord_induction_prop id succ_o g 0o ord_sum2).
 apply (ord_induction_unique p1 p2 ooa ob).
split; first by move=> x x0; rewrite ord_0_plus_unit_r //; ord_tac.
split; first by move=> x ox; rewrite ord_succ_pr //; ord_tac.
move=> x y oox ooy; rewrite /g.
set T:= fun_image _ _.
have ox: is_ordinal x by ord_tac.
have oy: is_ordinal y by ord_tac.
move: (ord_plus_normal ox); move=> [_ pn].
move: ordinal_one => oo.
case (limit_ordinal_pr2 oy).
  move: ooy=> [ooy _]; move: (zero_least_ordinal5 ooy); intuition.
case.
  move=> [z yz]; rewrite yz.
  have oT: ordinal_set T.
    move=> u; rewrite /T;aw; move=> [v]; rewrite ordinal_interval_pr //.
    move=>[[p3 p4]] <-.
    have ov: is_ordinal v by ord_tac.
    apply ordinal_succ; apply ord_sum2_ordinal => //.
  have oz: is_ordinal z by apply (elt_of_ordinal oy); rewrite yz /succ_o;fprops.
  have oxz: is_ordinal (ord_sum2 x z) by apply (ord_sum2_ordinal ox oz).
  rewrite -(ord_sum2_succ ox oz).
  apply ordinal_le_antisymmetric.
    apply ord_sup_pr3 => //; rewrite /T;aw; exists z; ee.
    move: ooy.
    rewrite (ordinal_interval_pr _ _ oy).
    rewrite {1} yz ord_lt_succ ord_succ_lt2 -yz=> ooy; ee; ord_tac.
  apply ord_sup_pr4 => //; first by fprops.
  move=> i; rewrite /T; aw. move=> [u [uv]] <-.
  rewrite - ord_succ_lt2 ord_lt_succ; apply ord_sum2_increasing1; try ord_tac.
  move: uv; rewrite (ordinal_interval_pr _ _ oy) yz ord_lt_succ; intuition.
move=> ly; rewrite (pn _ ly).
apply ord_sup_pr11;red;eee.
- move=> t; aw; move=> [z [zy]] <-; apply ord_sum2_ordinal => //.
  apply (elt_of_ordinal oy zy).
- move=> t; rewrite /T;aw; move=> [z [zy]] <-; apply ordinal_succ.
  apply ord_sum2_ordinal => //;apply (ordinal_interval_pr2 zy).
- move=> z; aw; move=> [u [uy xu]].
  case (equal_or_not u 0o) => unz.
    have ->: z = x by rewrite -xu unz ord_0_plus_unit_r //.
    exists (succ_o (succ_o x)); ee.
      rewrite /T;aw; exists 1o; ee.
        rewrite (ordinal_interval_pr _ _ oy); ee; first by ord_tac.
      apply f_equal; rewrite (ord_succ_pr ox) //.
      move:(ord_succ_lt ox) => [le1 _].
      have ox': is_ordinal (succ_o x) by ord_tac.
      move:(ord_succ_lt ox') => [le2 _]; ord_tac.
   exists (succ_o z).
   have ou:is_ordinal u by apply (elt_of_ordinal oy uy).
   have oz:is_ordinal z by rewrite -xu;apply ord_sum2_ordinal.
   split; last by move:(ord_succ_lt oz) => [le2 _].
   rewrite /T;aw; exists u; rewrite xu; ee.
   rewrite (ordinal_interval_pr _ _ oy);ee.
     apply zero_least_ordinal1 => //.
   rewrite ordinal_lt_pr0 //.
- move=> u; rewrite /T; aw. move => [v [viy uv]].
  move: (ordinal_interval_pr2 viy) => ov.
  move: (ord_sum2_ordinal ox ov) => os.
  have ou: is_ordinal u by rewrite - uv;apply ordinal_succ.
  exists u;split; last by ord_tac.
  aw; exists (succ_o v); split.
    move: ly =>[_[_ ly]]; apply ly; move: viy; rewrite ordinal_interval_pr //.
   rewrite ordinal_lt_pr0; intuition.
  by rewrite -(ord_sum2_succ ox ov).
Qed.

Lemma ord_induction_p14: forall a b,
  1o <=o a -> is_ordinal b ->
  ord_induction_defined (fun z:Set=> 0o) id ord_sum2 a b = a *o b.
Proof.
move=> a b oa1 ob.
set w0:= (fun z:Set=> 0o);set w1:= (fun z:Set=> z).
have oa: is_ordinal a by ord_tac.
have oax: ord_induction_axioms w1 ord_sum2 1o.
  split.
    move=> x xz;rewrite /w1; apply ordinal_le_reflexive; ord_tac.
  move=> x y x0 y0.
  have ox: is_ordinal x by ord_tac.
  have oy: is_ordinal y by ord_tac.
  split; first by apply ord_sum2_increasing2=> //.
  move=> h; move: (ordinal_a_ne_ab ox oy h).
  move: (zero_least_ordinal5 y0); intuition.
move: (ord_induction_exists w0 w1 ord_sum2 1o) => p1.
suff p2: (ord_induction_prop w0 w1 ord_sum2 1o ord_prod2).
 apply (ord_induction_unique p1 p2 oa1 ob).
split; first by move=> x x0; rewrite ord0_prodr //; ord_tac.
split; first by move=> x ox; rewrite /w1; rewrite ord_1_mult_unit_r //; ord_tac.
move=> x y ox1 oy1.
have ox: is_ordinal x by ord_tac.
have oy: is_ordinal y by ord_tac.
move: (ord_prod_normal ox (zero_least_ordinal5 ox1)); move=> [_ pn].
move: ordinal_one => oo.
case (limit_ordinal_pr2 oy).
  move: oy1=> [ooy _]; move: (zero_least_ordinal5 ooy); intuition.
set T:=fun_image _ _.
have oT: ordinal_set T.
  move=> t; rewrite /T;aw; move=> [z [zi]] <-.
  apply ord_sum2_ordinal =>//; apply ord_prod2_ordinal => //.
  apply (ordinal_interval_pr2 zi).
case.
  move=> [z yz]; rewrite yz.
  have oz: is_ordinal z by apply (elt_of_ordinal oy);rewrite yz /succ_o; fprops.
  have oxz: is_ordinal (ord_prod2 x z) by apply (ord_prod2_ordinal ox oz).
  have aux: ord_prod2 x (succ_o z) = ord_sum2 (ord_prod2 x z) x.
    rewrite -(ord_succ_pr oz) (order_sum_distributive3 oz ordinal_one ox).
    rewrite ord_1_mult_unit_r //.
  rewrite aux.
  move: (ord_sum2_ordinal oxz ox) => osp.
  apply ordinal_le_antisymmetric.
    apply ord_sup_pr3 => //; rewrite /T;aw; exists z; ee.
    rewrite (ordinal_interval_pr _ _ oy).
    rewrite yz; split; last by apply ord_succ_lt.
   apply zero_least_ordinal1 => //; move=> zz; move: oy1 =>[_].
   move: yz; rewrite zz succ_o_zero; move=> ->; intuition.
  apply ord_sup_pr4 => //.
  move=> i; rewrite /T; aw; move=> [u [uv]] <-.
  apply ord_sum2_increasing1; last by ord_tac.
  apply ord_prod2_increasing1; first by ord_tac.
  move: uv; rewrite ordinal_interval_pr // yz ord_lt_succ; intuition.
move=> ly; rewrite (pn _ ly).
apply ord_sup_pr11;red;eee.
- move=> t; aw; move=> [z [zy]] <-; apply ord_prod2_ordinal => //.
  apply (elt_of_ordinal oy zy).
- move=> z; aw; move=> [u [uy xu]].
  case (equal_or_not u 0o) => unz.
    have ->: z = 0o by rewrite -xu unz ord0_prodr //.
    set w := (ord_sum2 (ord_prod2 x 1o) x).
    have wT: inc w T.
      rewrite /w /T;aw;exists 1o;ee.
      rewrite ordinal_interval_pr; ee; ord_tac.
    by exists w;ee; apply zero_least_ordinal;apply oT.
  move: (elt_of_ordinal oy uy) => ou.
  exists (ord_sum2 (ord_prod2 x u) x); split.
    rewrite /T; aw; exists u;ee; rewrite ordinal_interval_pr; ee.
      apply zero_least_ordinal1 =>//.
    rewrite ordinal_lt_pr0;ee.
   rewrite -xu; apply ord_sum2_increasing2 =>//; apply ord_prod2_ordinal => //.
- move=> u; rewrite /T; aw; move => [v [viy uv]].
  move: (ordinal_interval_pr2 viy) => ov.
  move: (ord_prod2_ordinal ox ov) => os.
  move: (ord_sum2_ordinal os ox) => ou; rewrite uv in ou.
  exists u;split; last by ord_tac.
  aw; exists (succ_o v); split.
    move: ly =>[_[_ ly]]; apply ly; move: viy; rewrite ordinal_interval_pr //.
   rewrite ordinal_lt_pr0; intuition.
  rewrite -uv -(ord_succ_pr ov) order_sum_distributive3 // ord_1_mult_unit_r //.
Qed.

Definition ord_induction_axioms2 w1 g u :=
  ord_induction_axioms w1 g u &
  (forall a a', u <=o a -> a <o a' -> (w1 a) <o (w1 a')) &
  (forall a b a' b',
    u <=o a -> u <=o b -> a <=o a' -> b <=o b' ->
   (g a b) <=o (g a' b')).

Lemma ord_induction_p15: forall w0 w1 g u x y x' y',
  ord_induction_axioms2 w1 g u ->
   let f := ord_induction_defined w0 w1 g in
   u <=o x -> x <=o x' -> 1o <=o y -> y <=o y' -> f x y <=o f x' y'.
Proof.
move=> w0 w1 g u x y0 x' y' [oax [winc ginc]] f ux xx' y1 yy'.
have p1: (f x' y0) <=o (f x' y').
  have ux': u <=o x' by ord_tac.
  case (equal_or_not y0 y').
    move=> <-; apply ordinal_le_reflexive; apply (ord_induction_p5 oax ux' y1).
  move=> nyy'; have lyy': y0 <o y' by split.
  by move: (ord_induction_p8 w0 oax ux' y1 lyy')=> [aux _].
suff: (f x y0) <=o (f x' y0).
  move => p2; ord_tac.
ex_middle np0.
move: (ordinal_worder5 y1 np0 (p:= fun y=> (f x y) <=o (f x' y))) => /=.
set t := least_ordinal _ _; move=> [ot [t1 [pt lpy]]]; elim pt.
case (equal_or_not 1o t) => tn1.
  rewrite -tn1 /f !(ord_induction_p2 w0).
  case (equal_or_not x x') => lxx'.
    rewrite -lxx';move: oax=> [q1 q2]; move: (q1 _ ux) => q1x.
    apply ordinal_le_reflexive; ord_tac.
  have ltxx :x <o x' by split.
  by move: (winc _ _ ux ltxx) => [ok _ ].
have tlt1: 1o <o t by split.
have ux': u <=o x' by ord_tac.
move: (ord_induction_exists w0 w1 g u) => [_[_ ip]].
rewrite /f (ip _ _ ux tlt1)(ip _ _ ux' tlt1) -/f.
set T1:= fun_image _ _; set T2:= fun_image _ _.
have oT1: ordinal_set T1.
  move=> v; rewrite /T1; aw; move=> [z [zi]] <-.
  move: zi; rewrite ordinal_interval_pr //; move=>[h1 h2].
  apply (ord_induction_p6 oax ux h1).
have oT2: ordinal_set T2.
  move=> v; rewrite /T2; aw; move=> [z [zi]] <-.
  move: zi; rewrite ordinal_interval_pr //; move=>[h1 h2].
  apply (ord_induction_p6 oax ux' h1).
move: (ord_sup_pr1 oT2) => osT2.
apply (ord_sup_pr4 oT1 osT2).
move=> i; rewrite /T1;aw; move=> [z [z1 z2]].
move: (lpy _ z1) => h1.
move: (z1); rewrite (ordinal_interval_pr _ _ ot); move=> [ooz ozt].
move: (ord_induction_p41 w0 oax ux ooz); rewrite -/f => h3.
move: (ginc _ _ _ _ h3 ux h1 xx') => h4.
set j :=g (f x' z) x'.
have jT2: inc j T2 by rewrite /T2;aw; exists z; split.
move: (ord_sup_pr3 oT2 jT2)=> h5; rewrite -z2;ord_tac.
Qed.

Lemma ord_induction_p16: forall w0 w1 g u x y,
  ord_induction_axioms2 w1 g u ->
  u <=o x -> 1o <=o y ->
  let f := (ord_induction_defined w0 w1 g) in
    f x (succ_o y) = g (f x y) x.
Proof.
move=> w0 w1 g u x y oa2 ux y1 f.
move: (oa2)=> [oa1 [winc ginc]].
move: (ord_induction_exists w0 w1 g u) => [_[_ ip]].
have ooy:1o <o (succ_o y) by rewrite ord_lt_succ.
move: (ip _ _ ux ooy); rewrite -/f; move=> ->.
have oy: is_ordinal y by ord_tac.
move: (ordinal_succ oy)=> osy.
set T:= fun_image _ _.
have ox: is_ordinal x by ord_tac.
have lexx: x <=o x by ord_tac.
have oT: ordinal_set T.
  move=> v; rewrite /T; aw; move=> [z [zi]] <-.
  move: zi; rewrite ordinal_interval_pr //; move=>[h1 h2].
  apply (ord_induction_p6 oa1 ux h1).
move: (ord_induction_p6 (w0:=w0) oa1 ux y1); rewrite -/f => ogf.
apply ordinal_le_antisymmetric.
  apply (ord_sup_pr4 oT ogf).
  move=> i; rewrite /T; aw; move=> [z]; rewrite (ordinal_interval_pr _ _ osy).
  move=> [[oz olt1]] <-; rewrite -/f.
  rewrite ord_lt_succ in olt1.
  move: (ord_induction_p41 w0 oa1 ux oz); rewrite -/f => h3.
  move:(ord_induction_p15 w0 oa2 ux lexx oz olt1); rewrite -/f => ff.
  apply ginc => //.
apply (ord_sup_pr3 oT);rewrite /T; aw; exists y; ee.
rewrite (ordinal_interval_pr _ _ osy) ord_lt_succ; ee; ord_tac.
Qed.

Lemma ord_induction_p17: forall w0 w1 g u x x' y,
  ord_induction_axioms2 w1 g u ->
   (forall a b b', u <=o a -> u <=o b -> b <o b' -> g a b <o g a b') ->
   u <=o x -> x <o x' -> is_ordinal y ->
   let f := ord_induction_defined w0 w1 g in
   f x (succ_o y) <o f x' (succ_o y).
Proof.
move=> w0 w1 g u x x' y oa2 gsi ux xx' oy f.
move: (oa2) => [oa [winc ginc]].
case (equal_or_not y 0o) => yz.
  rewrite yz succ_o_zero.
  rewrite /f ! ord_induction_p2;apply winc => //.
have lexx' :ordinal_le x x' by move:xx' => [xx' _].
have lexx: ordinal_le x x by apply ordinal_le_reflexive; ord_tac.
have y1: ordinal_le 1o y by apply zero_least_ordinal1.
have ux':ordinal_le u x' by ord_tac.
have le1: ordinal_le (f x y) (f x' y).
  apply (ord_induction_p15 w0 oa2)=> //; ord_tac.
move: (ord_induction_p41 w0 oa ux y1); rewrite -/f => h3.
have le2: ordinal_le (g (f x y) x) (g (f x' y) x) by apply ginc =>//.
have l3: ordinal_lt (g (f x' y) x) (g (f x' y) x') by apply gsi=> //; ord_tac.
have le4 :ordinal_lt (g (f x y) x) (g (f x' y) x') by ord_tac.
rewrite /f (ord_induction_p16 w0 oa2 ux y1) (ord_induction_p16 w0 oa2 ux' y1).
done.
Qed.

Definition ord_induction_axioms3 w1 g u :=
  ord_induction_axioms2 w1 g u &
  (forall a, w1 a = a) &
  (forall a, u <=o a -> normal_ofs1 (fun b => g a b) u) &
  (forall a b c, u <=o a -> u <=o b -> u <=o c ->
     g (g a b) c = g a (g b c)).

Lemma ord_induction_p18: forall w0 w1 g u a b c,
  ord_induction_axioms3 w1 g u ->
  u <=o a -> 1o <=o b -> 1o <=o c ->
  let f := (ord_induction_defined w0 w1 g) in
    f a (b +o c) = g (f a b) (f a c).
Proof.
move=> w0 w1 g u a b c oa3 ua b1 c1 f.
ex_middle eqf.
set p:= fun y => f a (b +o y) = g (f a b) (f a y).
move: (ordinal_worder5 c1 eqf (p:=p)) => /=.
set t := least_ordinal _ _; move=> [ot [to1 [pt lpy]]]; elim pt; rewrite /p.
move: (oa3) => [oa2 [wu [gno gass]]].
move: (oa2) => [oa [winc ginc]].
case (equal_or_not 1o t) => t1.
  rewrite -t1 /p /f ord_induction_p2 wu.
  have ob: is_ordinal b by ord_tac.
  rewrite (ord_succ_pr ob).
  apply (ord_induction_p16 w0 oa2 ua b1).
case (limit_ordinal_pr2 ot).
  move => zt;move: (zero_least_ordinal5 to1); intuition.
case.
  move=> [y ty].
  have oy:is_ordinal y by apply (elt_of_ordinal ot); rewrite ty /succ_o; fprops.
  have ob: is_ordinal b by ord_tac.
  rewrite /p ty - (ord_sum2_succ ob oy).
  have yo:ordinal_le 1o y.
    apply zero_least_ordinal1 => //; dneg yz; rewrite ty yz succ_o_zero//.
  have byo:ordinal_le 1o (b +o y).
  move: (ord_sum2_increasing2 ob oy)=> aux; ord_tac.
  rewrite /f (ord_induction_p16 w0 oa2 ua yo) (ord_induction_p16 w0 oa2 ua byo).
  move:(ord_induction_p41 w0 oa ua b1)(ord_induction_p41 w0 oa ua yo).
  rewrite -/f => h h'; rewrite -(gass _ _ _ h h' ua).
  have lpyc: inc y (ordinal_interval 1o t).
    by rewrite ordinal_interval_pr // ty;ee; apply ord_succ_lt.
  by rewrite (lpy _ lpyc).
have t2: 1o <o t by split.
move=> tl.
move: (ord_induction_p10 w0 oa ua);rewrite normal_fs_equiv => nf1.
move: (nf1) => [nf4 nf5].
move:(ord_induction_p41 w0 oa ua b1).
rewrite /f (nf5 _ tl t2) -/f; move=> ufa.
move: (gno _ ufa)=> [gno2 gno3].
set X:= fun_image _ _ .
have neX: nonempty X.
  exists (f a 1o); rewrite /X; aw; exists 1o; ee.
  rewrite ordinal_interval_pr; ee; apply ordinal_le_reflexive; ord_tac.
have Xp: (forall x, inc x X -> u <=o x).
  move=> x; rewrite /X; aw; move=> [z [zi]] <-.
  move: zi; rewrite ordinal_interval_pr //;move => [z1 z2].
  apply (ord_induction_p41 w0 oa ua z1).
rewrite -(gno3 _ Xp neX).
set Y := fun_image _ _.
have ->:Y = fun_image (ordinal_interval 1o t) (fun z =>f a (ord_sum2 b z)).
  rewrite /Y /X;set_extens v; aw; move => [z [z1]] <-.
    move: z1; aw; move=> [w [wi]] <-; exists w;ee; apply (lpy _ wi).
  exists (f a z); split; first by aw; ex_tac.
  symmetry; apply (lpy _ z1).
have ob: is_ordinal b by ord_tac.
move: (ord_plus_normal ob) => [_ np]; rewrite (np _ tl).
move: (ord_induction_p10 w0 oa ua); rewrite -/f/normal_ofs1; move => [_ nf].
set X1 := (fun_image t (fun u0 : Set => ord_sum2 b u0)).
have neX1: nonempty X1.
  exists b; rewrite /X1;aw; exists 0o; ee.
    by move: tl => [_ [ok _]].
    rewrite ord_0_plus_unit_r //.
have X2: (forall x : Set, inc x X1 -> 1o <=o x).
  rewrite /X1;move=> x; aw; move=> [z [zt]] <-.
  move: (ord_sum2_increasing2 ob (elt_of_ordinal ot zt)) => aux; ord_tac.
symmetry;rewrite -(nf _ X2 neX1); apply ord_sup_pr13.
    move=> v; rewrite /X1; aw; move=> [z [zo]] <-.
    exists (b +o z); ee; aw; exists z; ee.
    move: zo; rewrite (ordinal_interval_pr _ _ ot).
    rewrite ordinal_lt_pr0; intuition.
  move=> v; aw; move=> [z [zX1]] <-.
  apply (ord_induction_p5 oa ua (X2 _ zX1)).
move=> v; aw; move=> [z []] ;rewrite /X1; aw; move=> [w [wt]] <- <-.
case (equal_or_not w 0o) => wnz.
  exists (f a (b +o 1o)); aw;ee.
    exists 1o;rewrite ordinal_interval_pr; ee.
    apply ordinal_le_reflexive;apply ordinal_1.
  rewrite wnz ord_0_plus_unit_r // (ord_succ_pr ob).
  move:(ord_succ_lt ob) => lt1.
  by move: (ord_induction_p8 w0 oa ua b1 lt1) => [res _].
exists (f a (b +o w)); aw; ee.
  exists w; ee; move: (elt_of_ordinal ot wt) => ow.
  rewrite (ordinal_interval_pr _ _ ot); rewrite ordinal_lt_pr0; ee.
  by apply zero_least_ordinal1.
apply ordinal_le_reflexive; apply (ord_induction_p5 oa ua).
move: (ord_sum2_increasing2 ob (elt_of_ordinal ot wt)) => aux; ord_tac.
Qed.

Lemma ord_induction_p19: forall w0 w1 g u a b c,
  ord_induction_axioms3 w1 g u ->
  u <=o a -> 1o <=o b -> 1o <=o c ->
  let f := (ord_induction_defined w0 w1 g) in
    f a (b *o c) = f (f a b) c.
Proof.
move=> w0 w1 g u a b c oa3 ua b1 c1 f.
ex_middle eqf.
set p:= fun y => f a (b *o y) = f (f a b) y.
move: (ordinal_worder5 c1 eqf (p:=p)) => /=.
set t := least_ordinal _ _; move=> [ot [to1 [pt lpy]]]; elim pt; rewrite /p.
move: (oa3) => [oa2 [wu [gno gass]]].
move: (oa2) => [oa [winc ginc]].
have ob: is_ordinal b by ord_tac.
case (equal_or_not 1o t) => t1.
  rewrite -t1 /p /f ord_induction_p2 wu.
  rewrite ord_1_mult_unit_r //.
move: (ord_induction_p41 w0 oa ua b1) => fab1.
case (limit_ordinal_pr2 ot).
  move => zt;move: (zero_least_ordinal5 to1); intuition.
case.
  move=> [y ty].
  have oy:is_ordinal y by apply (elt_of_ordinal ot); rewrite ty /succ_o; fprops.
  have oo: is_ordinal 1o by apply ordinal_1.
  have -> : (b *o t = ord_sum2 (b *o y) b).
    rewrite ty -(ord_succ_pr oy) (order_sum_distributive3 oy oo ob).
    rewrite ord_1_mult_unit_r //.
  have yo:ordinal_le 1o y.
    apply zero_least_ordinal1 => //; dneg yz; rewrite ty yz succ_o_zero//.
  move: (ord_prod2_increasing1 b1 yo); rewrite ord_1_mult_unit_r // => p1.
  move: (ord_induction_p18 w0 oa3 ua p1 b1) => /=. rewrite -/f.
  move=> ->.
  have lpyc: inc y (ordinal_interval 1o t).
    by rewrite ordinal_interval_pr // ty;ee; apply ord_succ_lt.
  rewrite (lpy _ lpyc) ty.
  move: (ord_induction_p16 w0 oa2 fab1 yo).
  by simpl; rewrite -/f; move=>->.
have t2: ordinal_lt 1o t by split.
move=> tl.
move: (ord_induction_p10 w0 oa fab1);rewrite normal_fs_equiv => nf1.
move: (nf1) => [_ nf5].
move:(ord_induction_p41 w0 oa ua b1).
rewrite /f (nf5 _ tl t2) -/f; move=> ufa; clear nf5.
set X:= fun_image _ _ .
have bnz: b <> 0o by apply zero_least_ordinal5.
move: (ord_prod_normal ob bnz) => [_ np]; rewrite (np _ tl).
move: (ord_induction_p10 w0 oa ua); rewrite -/f/normal_ofs1; move => [_ nf].
set X1 := fun_image _ _.
have oo: 1o <=o 1o.
  apply ordinal_le_reflexive;apply ordinal_1.
set X2:= fun_image (ordinal_interval 1o t) (fun u => ord_prod2 b u).
have ->: union X1 = union X2.
  symmetry; apply ord_sup_pr13.
      move=> v; rewrite /X1 /X2; aw; move=> [z [zo]] <-.
      exists z;ee; move: zo; rewrite (ordinal_interval_pr _ _ ot).
      rewrite ordinal_lt_pr0; intuition.
    move=> v; rewrite /X1; aw; move=> [z [zi]] <-.
    apply ord_prod2_ordinal => //; apply (elt_of_ordinal ot zi).
  rewrite /X1 /X2;move=> v; aw; move => [w [wt]] <-.
  case (equal_or_not w 0o) => wnz.
    exists b; ee.
      aw; exists 1o; rewrite ordinal_interval_pr;ee.
      rewrite ord_1_mult_unit_r //.
    by rewrite wnz (ord0_prodr ob); apply zero_least_ordinal.
  move: (elt_of_ordinal ot wt) => ow.
  exists (ord_prod2 b w); split.
    aw; exists w; ee.
    rewrite (ordinal_interval_pr _ _ ot); rewrite ordinal_lt_pr0; ee.
    by apply zero_least_ordinal1.
  apply ordinal_le_reflexive; apply (ord_prod2_ordinal ob ow).
have neX1: nonempty X2.
  exists b; rewrite /X2;aw; exists 1o; ee.
    rewrite (ordinal_interval_pr _ _ ot); ee.
  rewrite ord_1_mult_unit_r //.
have X2p: (forall x : Set, inc x X2 -> ordinal_le 1o x).
  rewrite /X2;move=> x; aw; move=> [z [zt]] <-.
  move: zt; rewrite (ordinal_interval_pr _ _ ot); move=> [oz _].
  move: (ord_prod2_increasing1 b1 oz); rewrite ord_1_mult_unit_r //.
  apply ordinal_1.
rewrite -(nf _ X2p neX1).
suff ->: X = (fun_image X2 (fun y : Set => f a y)) by [].
set_extens v; rewrite /X /X2; aw; move=> [z [zi]] <-.
  exists (ord_prod2 b z); ee; [ aw;exists z; ee | apply (lpy _ zi) ].
move: zi; aw; move=> [w [wi]] <-; ex_tac.
symmetry; apply: (lpy _ wi).
Qed.

Definition ord_pow a b :=
  Yo (a = 0o)
     (Yo (b = 0o) 1o 0o)
     (Yo (a = 1o) 1o
       (ord_induction_defined (fun z:Set => 1o) id ord_prod2
         a b)).
Notation "x ^o y" := (ord_pow x y) (at level 50).

Lemma ord2_lt_pr: forall x, 2o <=o x = 1o <o x.
Proof. by move=> x; rewrite /ord_two -succ_o_one - ord_succ_lt2. Qed.

Lemma ord_pow_axioms: ord_induction_axioms id ord_prod2 2o.
Proof.
split.
 move => x xe; apply ordinal_le_reflexive; ord_tac.
move=> x y x2 y2.
move: (ord2_trichotomy1 x2)(ord2_trichotomy1 y2)=> [p1 p2][p3 p4].
apply ord_mult_compat_lt1 =>//; ord_tac.
Qed.

Lemma ord_pow_axioms2: ord_induction_axioms2 id ord_prod2 2o.
Proof.
split; first by apply ord_pow_axioms.
split; first by [].
by move=> a b a' b' a2 b2 aa' bb'; apply ord_prod2_increasing1.
Qed.

Lemma ord_pow_axioms3: ord_induction_axioms3 id ord_prod2 2o.
Proof.
split; first by apply ord_pow_axioms2.
split; first by [].
split.
   move=> a a2.
   have aB: is_ordinal a by ord_tac.
   have anz: a <> 0o by move: (ord2_trichotomy1 a2) => [ok _].
   move: (ord_prod_normal aB anz).
   apply normal_fs_equiv2; apply ordinal_2.
move=> a b ta tb tc; symmetry;apply order_prod_assoc3; ord_tac.
Qed.

Lemma ord_pow00: 0o ^o 0o = 1o.
Proof. by rewrite /ord_pow; Ytac0; Ytac0. Qed.

Lemma ord_pow0x: forall x, x <> 0o -> 0o ^o x = 0o.
Proof. by move=> x xnz; rewrite /ord_pow; Ytac0; Ytac0. Qed.

Lemma ord_pow1x: forall x, 1o ^o x = 1o.
Proof.
have ooz: (1o <> 0o) by fprops.
by move=> x ; rewrite /ord_pow; Ytac0; Ytac0.
Qed.

Lemma ord_powx0: forall x, x ^o 0o = 1o.
Proof.
move=> x; rewrite /ord_pow.
Ytac xnz; [by Ytac0 | by Ytac xno => //; rewrite ord_induction_p1 ].
Qed.

Lemma ord_powx1: forall x, x ^o 1o = x.
Proof.
have zno: 1o <> 0o by fprops.
move=> x; rewrite /ord_pow; Ytac xz; [by Ytac0 |Ytac xno => // ].
by rewrite ord_induction_p2.
Qed.

Lemma ord_pow2x: forall x y, 2o <=o x ->
  x ^o y =
  ord_induction_defined (fun z:Set => 1o) id ord_prod2 x y.
Proof.
move=> x y x2; rewrite /ord_pow.
by move: (ord2_trichotomy1 x2) => [p1 p2]; Ytac0; Ytac0.
Qed.

Lemma ord_pow_ordinal: forall x y, is_ordinal x -> is_ordinal y ->
  is_ordinal (x ^o y).
Proof.
move=> x y ox oy.
case (ord2_trichotomy ox).
  move=> xz; case (equal_or_not y 0o) => yz.
   rewrite xz yz ord_pow00; apply ordinal_1.
  rewrite xz ord_pow0x //; apply ordinal_0.
case => xo; first by rewrite xo ord_pow1x; apply ordinal_1.
case (equal_or_not y 0o) => yz.
  rewrite yz; rewrite ord_powx0; apply ordinal_1.
have ooy: ordinal_le 1o y by apply zero_least_ordinal1.
rewrite (ord_pow2x y xo); apply (ord_induction_p5 ord_pow_axioms xo ooy).
Qed.

Lemma ord_pow_normal: forall x, 2o <=o x ->
  normal_ofs1 (fun y => x ^o y) 1o.
Proof.
move=> x x2; move: (ord_induction_p10 (fun z:Set => 1o) ord_pow_axioms x2).
set f := ord_induction_defined (fun _ : Set => 1o) ssrfun.id ord_prod2.
have op: forall y, ordinal_le 1o y -> ord_pow x y = f x y.
  by move=> y oy; apply ord_pow2x.
rewrite /normal_ofs1; move=> [p2 p3]; ee.
  move=> y1 y2 oy1 oyy.
  have oy2:ordinal_le 1o y2 by move: oyy => [aux _]; ord_tac.
  rewrite (op _ oy1) (op _ oy2); apply (p2 _ _ oy1 oyy).
move=> X Xp neX.
set Y:= (fun_image X (fun y : Set => ord_pow x y)).
have ->: Y = (fun_image X (fun y : Set => f x y)).
   set_extens t; rewrite /Y;aw; move=> [z [zX tv]]; rewrite -tv; ex_tac.
   by rewrite op //; apply Xp.
symmetry;rewrite (p3 _ Xp neX); apply op.
move: neX => [u ux]; move: (Xp _ ux) => uo.
have oX:ordinal_set X by move=> t tX; move: (Xp _ tX)=> aux; ord_tac.
move: (ord_sup_pr3 oX ux) => le2; ord_tac.
Qed.

Lemma ord_pow_increasing0: forall x y, 1o <=o x ->
  1o <=o y -> x <=o (x ^o y).
Proof.
move=> x y x2 y1.
case (equal_or_not 1o x) => o1.
  rewrite - o1 ord_pow1x; apply ordinal_le_reflexive; apply ordinal_1.
have o3: ordinal_le ord_two x by rewrite ord2_lt_pr; split.
move: (ord_induction_p4 (fun z:Set => 1o) ord_pow_axioms o3 y1).
rewrite ord_pow2x //.
Qed.

Lemma ord_pow_increasing1: forall x y , 2o <=o x ->
  is_ordinal y -> y <=o (x ^o y).
Proof.
move=> x y x2 y1.
case (equal_or_not y 0o) => yz.
  rewrite {1} yz; apply zero_least_ordinal;apply ord_pow_ordinal =>//; ord_tac.
have y2: ordinal_le 1o y by apply zero_least_ordinal1.
have x1: ordinal_le 1o x by move: x2; rewrite ord2_lt_pr; move=> [ok _].
move: (ord_induction_p9 (fun z:Set => 1o) ord_pow_axioms x2 x1 y2).
rewrite ord_pow2x //.
Qed.

Lemma ord_pow_increasing2: forall x y y', 2o <=o x ->
  y <o y' -> (x ^o y) <o (x ^o y').
Proof.
move=> x y y' x2 yy'.
have x3: ordinal_lt 1o x by move: x2; rewrite ord2_lt_pr.
have x1: ordinal_le 1o x by move: x3=> [ok _].
case (equal_or_not y 0o) => yz.
  rewrite yz ord_powx0.
  have oy1: ordinal_le 1o y'.
     apply zero_least_ordinal1; first by ord_tac.
     by move=> y'z; move: yy'; rewrite yz y'z; move=> [_ bad].
  move: (ord_pow_increasing0 x1 oy1) => le1; ord_tac.
have y1:ordinal_le 1o y by apply zero_least_ordinal1=>//; ord_tac.
move: (ord_induction_p8 (fun z:Set => 1o) ord_pow_axioms x2 y1 yy').
rewrite ord_pow2x // ord_pow2x //.
Qed.

Lemma ord_pow_increasing3: forall x y,
  is_ordinal x -> is_ordinal y -> x ^o y = 0o ->
  (x = 0o & y <> 0o).
Proof.
move=> x y ox oy pz.
case (equal_or_not y 0o).
  move=> h; move: pz; rewrite h; rewrite ord_powx0 => h'.
  by elim (card_one_not_zero).
move=> h1; ee.
case (equal_or_not x 0o) =>// xnz.
have xo: ordinal_le 1o x by apply zero_least_ordinal1.
have yo: ordinal_le 1o y by apply zero_least_ordinal1.
move: (ord_pow_increasing0 xo yo); rewrite pz; apply zero_least_ordinal3.
Qed.

Lemma ord_pow_increasing4: forall x x' y y',
  x <> 0o -> x <=o x' -> y <=o y' ->
  (x ^o y) <=o (x' ^o y').
Proof.
move=> x x' y y' xnz xx' yy'.
have ox': is_ordinal x' by ord_tac.
have oy': is_ordinal y' by ord_tac.
have p: ordinal_le 1o (ord_pow x' y').
  apply zero_least_ordinal1.
    by apply ord_pow_ordinal.
  move => pz; move: (ord_pow_increasing3 ox' oy' pz)=> [p1 p2].
  rewrite p1 in xx'; move: (zero_least_ordinal3 xx') => xz; contradiction.
case (equal_or_not x 1o) => x1; first by rewrite x1 ord_pow1x.
have ox: is_ordinal x by ord_tac.
have oy: is_ordinal y by ord_tac.
case (ord2_trichotomy ox); first by intuition.
case => x2;first by intuition.
case (equal_or_not y 0o) => yz; first by rewrite yz ord_powx0.
have y1: ordinal_le 1o y by apply zero_least_ordinal1.
move: (ord_induction_p15 (fun z:Set => 1o) ord_pow_axioms2 x2 xx' y1 yy').
rewrite ord_pow2x // ord_pow2x //; ord_tac.
Qed.

Lemma ord_pow_sum: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  a ^o (b +o c) = (a ^o b) *o (a ^o c).
Proof.
move=> a b c oa ob oc.
case (equal_or_not b 0o) => bz.
  rewrite bz ord_powx0 (ord_0_plus_unit_l oc) (ord_1_mult_unit_l) => //.
  apply ord_pow_ordinal => //.
case (equal_or_not c 0o) => cz.
  rewrite cz ord_powx0 (ord_0_plus_unit_r ob) (ord_1_mult_unit_r) => //.
  apply ord_pow_ordinal => //.
have b1: ordinal_le 1o b by apply zero_least_ordinal1.
have c1: ordinal_le 1o c by apply zero_least_ordinal1.
case (ord2_trichotomy oa) => az.
  rewrite az (ord_pow0x bz) (ord_pow0x cz) ord_pow0x.
    rewrite ord0_prodr => //; apply ordinal_zero.
  move=> sz; move: (ord_sum2_increasing2 ob oc); rewrite sz => bz1.
  elim bz;apply (zero_least_ordinal3 bz1).
case:az => az.
  rewrite az (ord_pow1x b) (ord_pow1x c)(ord_pow1x (ord_sum2 b c)).
  rewrite (ord_1_mult_unit_r) //; apply ordinal_1.
move: (ord_induction_p18 (fun z:Set => 1o) ord_pow_axioms3 az b1 c1).
rewrite (ord_pow2x b az)(ord_pow2x c az) (ord_pow2x (ord_sum2 b c) az) //.
Qed.

Lemma ord_pow_succ: forall x y, is_ordinal x -> is_ordinal y ->
  x ^o (succ_o y) = (x ^o y) *o x.
Proof.
move=> x y ox oy.
by rewrite -(ord_succ_pr oy) (ord_pow_sum ox oy ordinal_1) ord_powx1.
Qed.

Lemma ord_mult_succ: forall x y, is_ordinal x -> is_ordinal y ->
  x *o (succ_o y) = (x *o y) +o x.
Proof.
move=> x y ox oy.
rewrite -(ord_succ_pr oy) (order_sum_distributive3 oy ordinal_1 ox).
rewrite ord_1_mult_unit_r //.
Qed.

Lemma ord_pow_prod: forall a b c,
  is_ordinal a -> is_ordinal b -> is_ordinal c ->
  a ^o (b *o c) = (a ^o b) ^o c.
Proof.
move=> a b c oa ob oc.
case (equal_or_not b 0o) => bz.
  by rewrite bz (ord0_prodl oc) (ord_powx0 a) (ord_pow1x c).
case (equal_or_not c 0o) => cz.
  by rewrite cz (ord0_prodr ob) !ord_powx0.
have b1: ordinal_le 1o b by apply zero_least_ordinal1.
have c1: ordinal_le 1o c by apply zero_least_ordinal1.
case (ord2_trichotomy oa) => az.
  rewrite az (ord_pow0x bz) (ord_pow0x cz) ord_pow0x //.
  by apply ord_prod2_nz.
case:az => az.
  rewrite az (ord_pow1x b) (ord_pow1x c)(ord_pow1x (ord_prod2 b c)) //.
move: (ord_induction_p19 (fun z:Set => 1o) ord_pow_axioms3 az b1 c1).
simpl.
set f := ord_induction_defined (fun _ : Set => 1o) ssrfun.id ord_prod2.
rewrite (ord_pow2x b az)(ord_pow2x (ord_prod2 b c) az). rewrite -/f.
suff: (ordinal_le ord_two (f a b)).
  move => f2; rewrite (ord_pow2x c f2) //.
apply (ord_induction_p41 (fun _ : Set => 1o) ord_pow_axioms az b1).
Qed.

Lemma ord_pow_increasing5: forall a b,
  2o <=o a -> 1o <=o b -> (a *o b) <=o (a ^o b).
Proof.
move=> a b oa2 ob1.
ex_middle eqf.
move: (ord2_trichotomy1 oa2) => [pa1 pa2].
have oa: is_ordinal a by ord_tac.
have a1: ordinal_le 1o a by apply zero_least_ordinal1.
move: (ordinal_worder5 ob1 eqf
   (p:=fun z => ordinal_le (ord_prod2 a z)(ord_pow a z))) => /=.
set t := least_ordinal _ _; move=> [ot [to1 [pt lpy]]]; elim pt.
case (equal_or_not 1o t) => t1.
  rewrite -t1 ord_powx1 ord_1_mult_unit_r //; ord_tac.
case (limit_ordinal_pr2 ot).
  move => zt;move: (zero_least_ordinal5 to1); intuition.
case.
  move=> [y ty].
  have oy:is_ordinal y by apply (elt_of_ordinal ot); rewrite ty /succ_o; fprops.
  have oo: is_ordinal 1o by apply ordinal_1.
  rewrite ty (ord_pow_succ oa oy) (ord_mult_succ oa oy).
  move: (ord_pow_ordinal oa oy) => op.
  move: (ord_prod2_increasing1 (ordinal_le_reflexive op) oa2).
  rewrite (ord_double op)=> le1.
  have yo:ordinal_le 1o y.
    apply zero_least_ordinal1 => //; dneg yz; rewrite ty yz succ_o_zero//.
  have lpyc: inc y (ordinal_interval 1o t).
    by rewrite ordinal_interval_pr // ty;ee; apply ord_succ_lt.
  move: (lpy _ lpyc)=> le2.
  have au: ordinal_le a (ord_pow a y) by apply ord_pow_increasing0 =>//.
  move: (ord_sum2_increasing1 le2 au) => le3; ord_tac.
have t2: ordinal_lt 1o t by split.
move=> tl.
move: (ord_prod_normal oa pa1).
move=> [p2 p3]; rewrite (p3 _ tl).
move: (ord_pow_ordinal oa ot) => pato.
apply ord_sup_pr4.
    move=> u; aw; move=> [z [zt]] <-.
    apply (ord_prod2_ordinal oa (elt_of_ordinal ot zt)).
 exact.
move=> i; aw; move=> [z [zt]] <-.
case (equal_or_not z (0o)).
  move ->; rewrite (ord0_prodr oa); apply zero_least_ordinal => //.
move=> znz.
move: (elt_of_ordinal ot zt) => oz.
have lzt: ordinal_lt z t by rewrite - set_ord_lt_prop //.
have zi: inc z (ordinal_interval 1o t).
  by rewrite ordinal_interval_pr //;ee; apply zero_least_ordinal1.
move: (lpy _ zi)=> le1.
move: lzt=> [lezt _].
move: (ord_pow_increasing4 pa1 (ordinal_le_reflexive oa) lezt) => le2.
ord_tac.
Qed.

Definition ord_ext_div_pr (a b x y z: Set) :=
  is_ordinal x & is_ordinal y & is_ordinal z &
  b = ((a ^o x) *o y) +o z
  & z <o (a ^o x) & y <o a & y <> 0o.

Lemma ord_ext_div_unique: forall a b x y z x' y' z',
  2o <=o a -> 1o <=o b ->
  ord_ext_div_pr a b x y z -> ord_ext_div_pr a b x' y' z' ->
  (x=x' & y=y' & z=z').
Proof.
move=> a b x y z x' y' z' pa pb.
move => [ox [oy [oz [bv [r1 [r2 r3]]]]]][ox' [oy' [oz' [bv' [r1' [r2' r3']]]]]].
set q:= (ord_pow a x) in bv r1.
set q':= (ord_pow a x') in bv' r1'.
have oq: is_ordinal q by ord_tac.
have oq': is_ordinal q' by ord_tac.
have oa: is_ordinal a by ord_tac.
move: ordinal_1 => oo.
have qb: ordinal_le q b.
  move: (ord_prod2_increasing2 oq oy r3) => qy.
  have oqy: is_ordinal (ord_prod2 q y) by ord_tac.
  move:(ord_sum2_increasing2 oqy oz).
  rewrite -bv; move=> h; ord_tac.
have qb': ordinal_le q' b.
  move: (ord_prod2_increasing2 oq' oy' r3') => qy.
  have oqy: is_ordinal (ord_prod2 q' y') by ord_tac.
  move:(ord_sum2_increasing2 oqy oz').
  rewrite -bv'; move=> h; ord_tac.
move: (ord_prod2_ordinal oq oy) => oqy.
move: (ord_prod2_ordinal oq' oy') => oqy'.
have sqb: ordinal_lt b (ord_pow a (succ_o x)).
  rewrite (ord_pow_succ oa ox) -/q.
  have p2:(ordinal_le q q) by ord_tac.
  move: r2; rewrite ord_succ_lt2 => p1.
  move: (ord_prod2_increasing1 p2 p1).
  rewrite (ord_mult_succ oq oy) => le1.
  move: (ord_plus_compat_lt r1 oqy).
  rewrite -bv; move=> le2; ord_tac.
have sqb': ordinal_lt b (ord_pow a (succ_o x')).
  rewrite (ord_pow_succ oa ox') -/q'.
  move: r2'; rewrite ord_succ_lt2 => p1.
  have p2:(ordinal_le q' q') by ord_tac.
  move: (ord_prod2_increasing1 p2 p1).
  rewrite (ord_mult_succ oq' oy') => le1.
  move: (ord_plus_compat_lt r1' oqy').
  rewrite -bv'; move=> le2; ord_tac.
have od: ord_div_pr0 b q y z by red; ee.
have od': ord_div_pr0 b q' y' z' by red; ee.
suff xx': x = x'.
   have qq': q = q' by rewrite /q /q' xx'.
   rewrite -qq' in od'.
   have ob: is_ordinal b by ord_tac.
   move: (ord_division_unique ob oq od od').
   intuition.
have a1: ordinal_le 1o a.
   by move: (ord2_trichotomy1 pa) => [pa1 pa2]; apply zero_least_ordinal1.
case (equal_or_not x 0o) => xz.
  case (equal_or_not x' 0o) => xz'.
    by rewrite xz xz'.
  have q1: q = 1o by rewrite /q xz ord_powx0.
  have z0: z = 0o.
    move: r1; rewrite q1 => p1.
    ex_middle zzo; move: (zero_least_ordinal1 oz zzo) => p2; ord_tac.
  have ltba: ordinal_lt b a.
    rewrite bv z0 (ord_0_plus_unit_r oqy) q1 (ord_1_mult_unit_l oy) //.
  have x1: ordinal_le 1o x' by apply zero_least_ordinal1.
  move: (ord_pow_increasing0 a1 x1); rewrite -/q' => le3.
  move: (ordinal_le_transitive le3 qb') => le4; ord_tac.
case (equal_or_not x' 0o) => xz'.
  have q1: q' = 1o by rewrite /q' xz' ord_powx0.
  have z0: z' = 0o.
    move: r1'; rewrite q1 => p1.
    ex_middle zzo; move: (zero_least_ordinal1 oz' zzo) => p2; ord_tac.
  have ltba: ordinal_lt b a.
    rewrite bv' z0 (ord_0_plus_unit_r oqy') q1 (ord_1_mult_unit_l oy') //.
  have x1: ordinal_le 1o x by apply zero_least_ordinal1.
  move: (ord_pow_increasing0 a1 x1); rewrite -/q => le3.
  move: (ordinal_le_transitive le3 qb) => le4; ord_tac.
have x1: ordinal_le 1o x by apply zero_least_ordinal1.
have x1': ordinal_le 1o x' by apply zero_least_ordinal1.
move: qb sqb qb' sqb'.
rewrite /q /q' !(ord_pow2x _ pa).
set f := ord_induction_defined _ _ _.
apply (ord_induction_p11 ord_pow_axioms pa x1 x1').
Qed.

Lemma ord_ext_div_exists: forall a b,
  2o <=o a -> 1o <=o b ->
  exists x, exists y, exists z, ord_ext_div_pr a b x y z.
Proof.
move=> a b a2 b1.
have oa: is_ordinal a by ord_tac.
have ob: is_ordinal b by ord_tac.
case (ordinal_le_total_order1 oa ob); last first.
  move=> ba; exists 0o; exists b; exists 0o; red.
  rewrite (ord_powx0 a) (ord_1_mult_unit_l ob)(ord_0_plus_unit_r ob).
  move: ordinal_0 => o0; ee; [apply ord_lt_01 | by apply zero_least_ordinal5].
move=> ab.
set w1:= fun z:Set => z.
have w1a: ordinal_le (w1 a) b by [].
have a1: ordinal_le 1o a.
 by move: (ord2_trichotomy1 a2) => [pa1 pa2]; apply zero_least_ordinal1.
pose w0 (_ : Set) := 1o.
move: (ord_induction_p12 w0 ord_pow_axioms a2 w1a a1) => /=; move=> [y].
rewrite -(ord_pow2x y a2) -(ord_pow2x (succ_o y) a2).
move=> [ooy [yb [fyb fysb]]].
have oy: is_ordinal y by ord_tac.
move: fysb; rewrite (ord_pow_succ oa oy).
move:(ord_pow_ordinal oa oy)=> oay ltb.
move: (ord_division_exists ob oay oa ltb)=> [q [r [[oq [or [abq lt1]]] lt2]]].
exists y; exists q; exists r; red; ee.
move=> qz; move: abq; rewrite qz (ord0_prodr oay) (ord_0_plus_unit_l or).
move=> h; rewrite h in fyb; ord_tac.
Qed.