proposition: Lemma ord_lt_irrefl: forall alpha:Ordinal, ~(alpha < alpha).
proof: Proof. intro; red; intro. assert (forall beta:Ordinal, beta <> alpha). { intro. pose proof (ordinals_well_founded beta). induction H0. red; intro. symmetry in H2; destruct H2. contradiction (H1 alpha H); trivial. } contradiction (H0 alpha); trivial. Qed.
imports: Coq(Classical) Coq(Eqdep)