proposition: Theorem increasing_stationaryP r: order r -> ((forall X, sub X (substrate r) -> nonempty X -> exists a, maximal (induced_order r X) a) <-> (forall f, increasing_sequence f r -> stationary_sequence f)).
proof: Proof. move=> or;split. move=> hyp f [fgf df rf incf]; rewrite /stationary_sequence;split => //. have ner: (nonempty (range f)). exists (Vg f \0c); apply: (inc_V_range fgf); rewrite df; apply:NS0. move: (hyp _ rf ner) => [a];rewrite /maximal iorder_sr //. move => [ha]; move: (ha) => /(range_gP fgf) [x pa eq] alv; rewrite df in pa. exists x => // n nN xn. move: (incf _ _ pa nN xn); rewrite -eq => h; apply: alv. apply / iorder_gle0P => //; apply /(range_gP fgf); exists n=> //; ue. move=> h X Xsr neX. pose T x := Zo X (fun y => glt r x y). case: (emptyset_dichot (productb (Lg X T))) => pe. have [x xX Tx]: (exists2 x, inc x X & T x = emptyset). ex_middle eh. have p1: (fgraph (Lg X T)) by fprops. have p2: (forall i, inc i (domain (Lg X T)) -> nonempty (Vg (Lg X T) i)). aw;move=> i iX; rewrite LgV// ;case: (emptyset_dichot (T i))=> //ie. case: eh; ex_tac. by move: (setXb_ne p2); rewrite pe; move /nonemptyP. exists x;split => //; first by rewrite iorder_sr //. move => t xt; move:(iorder_gle1 xt) => xt1. move: (iorder_gle3 xt) => [_ tX]. ex_middle w; empty_tac1 t; apply: Zo_i =>//; split;fprops. move:pe=> [y yp]. have p1: (forall x, inc x X -> glt r x (Vg y x)). have aux: fgraph (Lg X T) by fprops. move: yp => /setXb_P;aw; move => [pa pb pc] x xX. by move: (pc _ xX); rewrite LgV // =>/Zo_P []. have p2: (forall x, inc x X -> inc (Vg y x) X). have aux: fgraph (Lg X T) by fprops. move: yp => /setXb_P; aw; move => [pa pb pc] x xX. by move: (pc _ xX); rewrite LgV // =>/Zo_P []. move:neX => [y0 y0X]. move: (integer_induction_stable y0X p2). move:(induction_defined_pr (Vg y) y0); simpl. set f:= induction_defined _ _. move=> [sf [ff _] f0 fn] tfX. have p3: (forall n, natp n -> glt r (Vf f n) (Vf f (csucc n))). move=> n nN; rewrite fn //; apply: p1; apply: tfX; Wtac; ue. have p4: (forall n, natp n -> gle r (Vf f n) (Vf f (csucc n))). by move=> n nN; move: (p3 _ nN)=> [ok _]. have s2: sub (target f) (substrate r) by apply: (sub_trans tfX). move:(h _ (increasing_seq_prop or ff sf s2 p4)) => [_ _ [m mN sm]]. have sN: natp (csucc m) by fprops. move: (sm _ sN (cleS mN)); move: (p3 _ mN); rewrite /Vf. by move=> /proj2 h1 h2; move: h1; rewrite h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)