proposition: Theorem decreasing_stationaryP r: total_order r -> ((worder r) <-> (forall f, decreasing_sequence f r -> stationary_sequence f)).
proof: Proof. move=> tor; split => hyp. move=> 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=> [or wor]; move: (wor _ rf ner) => [y []]; rewrite iorder_sr//. move /(range_gP fgf) => [x xdf xv] hb. rewrite df in xdf. exists x => // n nN xn. move: (incf _ _ xdf nN xn) => pa. have hh: inc (Vg f n) (range f) by apply /(range_gP fgf); exists n => //; ue. move: (iorder_gle1 (hb _ hh)); rewrite xv => leq1; order_tac. set (r':= opp_order r). have or: order r by move: tor => [or _]. move: (opp_osr or) => [or' sr']. split =>// x xsr nex. have la:= (total_order_lattice (total_order_sub tor xsr)). have srsr': (substrate r = substrate r') by rewrite sr'. have aux: (forall f, increasing_sequence f r' -> stationary_sequence f). move=> f fi; apply: hyp; move : fi => [p1 p2 p3 p4]; split => //; try ue. move=> n m nN mN nm; move: (p4 _ _ nN mN nm); rewrite /r'. by move /igraph_pP. move: (iorder_osr or xsr) => [oi soi]. move: aux; move /(increasing_stationaryP or'); rewrite - srsr' => aux. move: (aux _ xsr nex) => [a]; rewrite /r' (iorder_opposite x or). move/(maximal_opp oi) => mi. exists a; apply: (left_directed_minimal (proj2 (lattice_directed la)) mi). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)