proposition: Theorem noetherian_induction r F: order r -> (forall X, sub X (substrate r) -> nonempty X -> exists a, maximal (induced_order r X) a) -> sub F (substrate r) -> (forall a, inc a (substrate r) -> (forall x, glt r a x -> inc x F) -> inc a F) -> F = substrate r.
proof: Proof. move=> or p1 p2 p3. set (c := (substrate r) -s F). case: (emptyset_dichot c) => ce. apply: extensionality => //; move=> x xsr; ex_middle xsf. empty_tac1 x; apply /setC_P;split => //. have cs: sub c (substrate r) by rewrite /c; apply: sub_setC. move: (p1 _ cs ce) => [a]; rewrite / maximal iorder_sr//; move => [ac am]. have aux: (forall y, glt r a y -> inc y F). move=> y xy; ex_middle w. have yc: (inc y c) by apply /setC_P;split => //; order_tac. move: xy => [xy nxy]; case: nxy. have ham: gle (induced_order r c) a y by apply /iorder_gleP. by rewrite (am _ ham). by move: (p3 _ (cs _ ac) aux); move: ac => /setC_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)