proposition: Lemma total_order_worder_dichot r: total_order r -> (worder r \/ exists f, decreasing_strict_sequence f r).
proof: Proof. move => tor. move:(decreasing_stationaryP tor) => H. case: (p_or_not_p (worder r)) => ha; [by left | right]. ex_middle hb; case: ha; apply/H => f [qa qb qc qd]; split => //. ex_middle hc; case hb. pose Z n := Zo Nat (fun m => n <c m /\ glt r (Vg f m) (Vg f n)). have sif: forall n, natp n -> nonempty (Z n). move => n nN; apply /nonemptyP => ze; case hc; exists n => // m mN lemn. move: (qd _ _ nN mN lemn) => ha; ex_middle he; empty_tac1 m. by apply Zo_i => //; split => //; split => // hf; case he; rewrite hf. pose F n := intersection (Z n). have Fp: forall n, natp n -> [/\ natp (F n), n <c (F n) & glt r (Vg f (F n)) (Vg f n)]. move => n nN. have sN: sub (Z n) Nat by apply:Zo_S. by move: (proj1 (inf_Nat sN (sif _ nN))) => /Zo_P [hu [hv hw]]. move: (induction_defined_pr F \0c) =>[]. set g := (induction_defined F \0c). move => sg sjg g0 gs. have gN: forall n, natp n -> natp (Vf g n). apply: Nat_induction; first by rewrite g0; apply:NS0. by move => n nN hr; rewrite (gs _ nN); exact: (proj31 (Fp _ hr)). pose h n := Vg f (Vf g n). have hr: forall n, natp n -> glt r (h (csucc n)) (h n) . move => n nN; rewrite /h (gs _ nN); exact:(proj33 (Fp _ (gN _ nN))). have fgh: fgraph (Lg Nat h) by fprops. exists (Lg Nat h); saw. move => t /(range_gP fgh); aw; move => [z zN ->]; rewrite LgV//. move : (proj1 (hr _ zN)) => le1; order_tac. move => n m nN mN nm. rewrite - (cdiff_pr (proj1 nm)). move:(NS_diff n mN) (cdiff_nz nm). move:(m -c n); clear mN nm m; apply: Nat_induction => //. move => m mN Ha _. have sN:= NS_sum nN mN. have sN1:= (NS_succ sN). rewrite (csum_nS _ mN) /h !LgV// (gs _ sN). case: (equal_or_not m \0c). move => ->; rewrite (csum0r (CS_nat nN)). exact: (proj33 (Fp _ (gN _ nN))). move /Ha; move:(proj33 (Fp _ (gN _ sN))); rewrite /h !LgV //. move => pa pb; exact: (lt_lt_trans (proj1 tor) pa pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)