proposition: Lemma wo_induction : forall (a : E) (H : is_well_ordered a) (p : EP), (forall x : E, inc x (U a) -> (forall y : E, inc y (U a) -> lt a y x -> p y) -> p x) -> forall x : E, inc x (U a) -> p x.
proof: Proof. ir. set (b := Z (U a) (fun z : E => ~ p z)). ap excluded_middle; uf not; ir. assert (nonempty b). apply nonempty_intro with x. uf b. Ztac. set (z := choose_bottom_element a b). assert (is_bottom_element a b z). uf z; ap wo_choose_bottom. am. uf b; ap Z_sub. am. assert (sub b (U a)). uf b; ap Z_sub. assert (inc z b). ufi is_bottom_element H4; ee. assert (inc z (U a)). ap H5; am. am. assert (~ p z). ufi b H6. Ztac. ap H7. ap H0; ir. au. ap excluded_middle; uf not; ir. assert (inc y b). uf b; Ztac. apply bottom_element_no_lt with a b z y; au. Qed.
imports: universe