proposition: Lemma ordinals_well_founded: well_founded ord_lt.
proof: Proof. red; intro alpha. induction alpha. constructor. intros beta ?. apply ord_le_respects_succ_converse in H. constructor; intros gamma ?. destruct IHalpha. apply H1. apply ord_lt_le_trans with beta; trivial. constructor; intros alpha ?. apply ord_le_S_sup_converse in H0. destruct H0 as [j]. destruct (H j). apply H1; trivial. Qed.
imports: Classical