proposition: Theorem transfinite_induction (P: Ord->Prop) : progressive P -> forall a, P a.
proof: Proof. intros Hp; case (classic (forall a : Ord, P a)); [trivial|idtac]. intro H; case (not_all_ex_not _ (fun a => P a) H). intros x Hx. assert False. { case (well_order (fun z => ~ P z) _ Hx (WO := AX1)). intros x0 H0; assert (forall b, b < x0 -> P b). { intros. case H0; intros H3 H5; apply NNPP. intro H6. case (H5 _ H6). intro;subst x0. case (Lt_irreflexive (a:=b));auto. intro; case (Lt_irreflexive (a:=b)). eapply Lt_trans; eauto. exact AX1. } assert (~ (P x0)) by (case H0; unfold In; tauto). apply H2; apply Hp;auto. } contradiction. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)