proposition: Lemma Exercise6_29d r X: order r -> finite_set X -> (forall x, inc x X -> Noetherian_set r x) -> Noetherian_set r (union X).
proof: Proof. move => or; move: X. apply: (finite_set_induction). move => _; rewrite setU_0; apply: Exercise6_29b. move => a n Hrec aux. have ->: union (a +s1 n) = (union a) \cup n. set_extens t. move => /setU_P [y ty] /setU1_P; case => h; apply /setU2_P; [ left;union_tac | right; ue]. case /setU2_P. move /setU_P=> [y ty ya]; union_tac. by move => tn; apply /setU_P;exists n;fprops. apply: (Exercise6_29c or); last by apply: aux; fprops. apply: Hrec=> x xa; apply: aux; fprops. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)