proposition: Lemma Exercise6_29e r X: order r -> Noetherian r -> sub X (substrate r) -> Noetherian_set r X.
proof: Proof. move => or Nr xsr. rewrite (Noetherian_set_pr or xsr) => Y YX neY. move: (sub_trans YX xsr) => Ysr. move: (Nr _ Ysr neY) => [a []]. rewrite (iorder_sr or Ysr) => pa pb. by ex_tac; move => x xY ax; apply: pb; apply /iorder_gleP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)