proposition: Lemma Exercise6_29f r: order r -> (Noetherian r <-> (forall i, inc i (substrate r) -> Noetherian_set r (interval_ou r i))).
proof: Proof. move => or; split => h. by move => i isr; apply: (Exercise6_29e or h); apply: Zo_S. move => X Xsr neX. move: (neX) => [a aX]. case: (p_or_not_p (maximal (induced_order r X) a)) => ma. by exists a. set Y := Zo X (fun z => glt r a z). case: (emptyset_dichot Y) => neY. case: ma; split; first by rewrite (iorder_sr or Xsr). move => x /iorder_gleP [_ pa pb]. by ex_middle exa; empty_tac1 x; apply: Zo_i=> //; split => //; apply: nesym. have sY: sub Y (interval_ou r a). move => y /Zo_P [yX ay]; apply /Zo_P; split => //; order_tac. fprops. move: (h _ (Xsr _ aX)). have Isr: sub (interval_ou r a) (substrate r) by apply: Zo_S. rewrite (Noetherian_set_pr or Isr) => aux. move: (aux _ sY neY) => [b ibY etc]. move: ibY => /Zo_P [bX ab]. exists b; split; first by rewrite (iorder_sr or Xsr). move=> x /iorder_gleP [_ xX bx]. apply: etc => //;apply /Zo_P; split => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)