proposition: Lemma well_ordering_pair: worder_r ord_pair_le.
proof: Proof. move: ordering_pair4 => or1. have oR: reflexive_rr ord_pair_le. by move => x y [p1 p2 _]; split; apply: or1. have oA: antisymmetric_r ord_pair_le. move => x y [p1 p2 p3] [_ _ q3]; case: p3 => p3; case: q3 => q3. + by move: q3 => [q3 _]; case: (oltNge p3 q3). + by move: q3 => [q3 _]; rewrite q3 in p3; case: p3. + by move: p3 => [p3 _]; rewrite p3 in q3; case: q3. + move: p3 => [p31 p32]; move: q3 => [q31 q32]. case: p32 => p32; case: q32 => q32. - by move: q32 => [q32 _];case: (oltNge p32 q32). - by move: q32 => [q32 _]; rewrite q32 in p32; case: p32. - by move: p32 => [p32 _]; rewrite p32 in q32; case: q32. - move: p32 => [pa pb]; move: q32 => [_ pc]. move: p1 p2 => [px _ _][py _ _]; apply: pair_exten => //. by apply:oleA pb pc. split. split => //. move => a b c [p1 p2 p3] [q1 q2 q3]. split ; [exact | exact | ]. case: p3 => p3; case: q3 => q3. - by left; apply: (olt_ltT p3 q3). - move: q3 => [q3a q3b];case: q3b => q3b; first by rewrite q3a in p3; left. move: q3b => [q4 q5]; left;ue. - by move: p3 => [p31 p32]; rewrite -p31 in q3; left. - move: p3 q3 => [p3 p4] [q3 q4]; right; split => //; first by ue. case:p4=> p4. left; case: q4; move => [q4 q5]; [ apply:olt_leT p4 q4 |ue ]. move: p4 => [ -> p4]. case: q4; [by left| move=> [p5 p6];right;split => //;apply:oleT p4 p6]. move => x cx [x0 x0x]. set S1:= fun_image x ord_pair_max. have os1: ordinal_set S1. by move=> t /funI_P [z zx ->]; apply:ordering_pair2; move/cx: zx => []. have nes1: nonempty S1 by exists (ord_pair_max x0); apply /funI_P; ex_tac. move: (ordinal_setI nes1 os1); set gamma:= intersection S1 => gs1. have g1: forall z, inc z x -> gamma <=o (ord_pair_max z). move => z zx. have aa: inc (ord_pair_max z) S1 by apply /funI_P; ex_tac. move: (os1 _ aa) => ou; split => //. by apply os1. by apply: setI_s1. move: gs1 => /funI_P [g0 g0x g0v]. set S2:= fun_image (Zo x (fun z => ord_pair_max z = gamma)) P. have nes2: nonempty S2. by apply: funI_setne; exists g0 => //; apply: Zo_i. have os2: ordinal_set S2. move =>t /funI_P [z /Zo_S zx ->]. by move: (cx _ zx) => [[ _ aa _] _ _]. move: (ordinal_setI nes2 os2); set alpha:= intersection S2 => as1. have a1: forall z, inc z x -> gamma <o (ord_pair_max z) \/ (gamma = ord_pair_max z) /\ alpha <=o P z. move=> z zx; move: (g1 _ zx) => le1. case: (equal_or_not gamma (ord_pair_max z)) => eq; last by left. have pa: inc (P z) S2 by apply/funI_P; exists z => //; apply: Zo_i => //. by right;split => //; hnf; split; fprops;apply: setI_s1. move: as1 => /funI_P [a0 /Zo_P [a0x ba] qa]. set S3 := fun_image (Zo x (fun z => (ord_pair_max z) = gamma /\ (P z) = alpha)) Q. have neS3: nonempty S3. by apply: funI_setne; exists a0 => //; apply: Zo_i. have os3: ordinal_set S3. move =>t /funI_P [z /Zo_P [pa _] ->]. by move: (cx _ pa) => [[_ qb qc] _]. move: (ordinal_setI neS3 os3); set beta:= intersection S3 => as2. move: as2 => /funI_P [b0 /Zo_P [b0x [pd pb]] pc]. exists b0; hnf. rewrite (graph_on_sr cx); split => //. move=> t tx; apply /graph_on_P1;split => //;split => //. by move: (cx _ b0x) => [ok _]. by move: (cx _ tx) => [ok _]. case: (a1 _ tx); first by rewrite pd => h; left. rewrite pd; move=> [pe pf]; right; split => //. rewrite pb; case: (equal_or_not alpha (P t)) => eq1; last by left. right; split => //; hnf; split => //. by move: (cx _ b0x) => [[_ _ ra] _]. by move: (cx _ tx) => [[_ _ ra] _]. have pg: inc (Q t) S3 by apply/funI_P; exists t => //; apply: Zo_i => //. rewrite - pc; apply (setI_s1 pg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)