proposition: Lemma Noetherian_set_pr r x: order r -> sub x (substrate r) -> (Noetherian_set r x <-> (forall X, sub X x -> nonempty X -> exists2 a, inc a X & (forall x, inc x X -> gle r a x -> x = a))).
proof: Proof. move => or xsr; rewrite /Noetherian_set /Noetherian. rewrite (iorder_sr or xsr); split. move => [_ h] X Xx xne; move: (h _ Xx xne);rewrite (iorder_trans _ Xx). move=> [a []]; rewrite (iorder_sr or (sub_trans Xx xsr)) => ax ap. by ex_tac; move => t tX lat; apply: ap; apply /iorder_gleP. move => h; split; first exact. move => X Xx ne; rewrite (iorder_trans _ Xx); move: (h _ Xx ne) => [a ax ap]. exists a; split; first by rewrite (iorder_sr or (sub_trans Xx xsr)). by move => b => /iorder_gleP [_ bx ab]; apply: ap. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)