proposition: Lemma Exercise6_29c r a b: order r -> Noetherian_set r a -> Noetherian_set r b -> Noetherian_set r (a \cup b).
proof: Proof. move => or pa pb. move: (proj1 pa) (proj1 pb) => asr bsr. move/(Noetherian_set_pr or asr):pa => pa. move /(Noetherian_set_pr or bsr):pb => pb. have usr: sub (a \cup b) (substrate r) by move=> t; case /setU2_P; [apply asr | apply: bsr]. apply/ (Noetherian_set_pr or usr). move => X Xu neX. set Xa:= X \cap a. case: (emptyset_dichot Xa) => Xane. have sb: sub X b. move => t tX; move: (Xu _ tX); case /setU2_P => // ta. by empty_tac1 t; apply /setI2_P. by apply: pb. have sxa: sub Xa a by apply: subsetI2r. move: (pa _ sxa Xane) => [ea sea eap]. set Xb:= Zo X (fun t => glt r ea t). case: (emptyset_dichot Xb) => Xbne. have eax: inc ea X by move: sea;move /setI2_P=> []. exists ea => //; move => x xE le1; ex_middle ne. by empty_tac1 x; apply: Zo_i => //;split => //; apply:nesym. have sxb: sub Xb b. move => t /Zo_P [tx [le1 ne1]]. move: (Xu _ tx);case /setU2_P=> // ta. have txa: inc t Xa by rewrite /Xa; fprops. by move: (eap _ txa le1) =>eq1; case: ne1. move: (pb _ sxb Xbne) => [eb seb ebp]. have ebx: inc eb X by move: seb => /Zo_P []. exists eb => //; move => x xE le1. apply: ebp => //; apply: Zo_i => //. move: seb => /Zo_P [_ lt1]; order_tac. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)