proposition: Theorem lt_irrefl : forall x, ~lt x x.
proof: Proof. assert (Hin : forall x y, lt x y -> x = between_cst \/ x = false_cst \/ x = ge_cst \/ x = le_cst) by (intros x y H; elim H; auto). assert (Hin' : forall x y, lt x y -> y = false_cst \/ y = ge_cst \/ y = le_cst \/ y = true_cst) by (intros x y H; elim H; auto). assert (Hle : forall x y, lt x y -> x = le_cst -> y = true_cst). intros x y H; elim H; try (intros; discriminate); auto. intros x' y' z Hxy Hi1 Hyz Hi2 Hx; rewrite Hi1 in Hyz; auto. destruct (Hin _ _ Hyz) as [H' | [H' | [H' | H']]]; discriminate H'. assert (Hin2 : forall x y, lt x y -> forall z, lt y z -> x = between_cst \/ x = false_cst \/ x = ge_cst). intros x y H; elim H; eauto. intros z Hz; destruct (Hin _ _ Hz) as [H' | [ H' | [H'|H']]];discriminate H'. assert (Hin3 : forall x y, lt x y -> forall z, lt y z -> forall u, lt z u -> x = between_cst \/ x = false_cst). intros x y H; elim H; clear H; eauto. intros z Hz; assert (Hle' := Hle _ _ Hz); rewrite Hle'; auto. intros u Hu; assert (Hin'' := Hin _ _ Hu). destruct Hin'' as [H' | [H' | [H' | H']]]; discriminate H'. intros z Hz; assert (Hin'' := Hin _ _ Hz). destruct Hin'' as [H' | [H' | [H' | H']]]; discriminate H'. assert (Hin4 : forall x y, lt x y -> forall z, lt y z -> forall u, lt z u -> forall v, lt u v -> x = between_cst). intros x y H; elim H; clear H; eauto. intros z Hz; inversion Hz. intros u Hu; assert (u = true_cst) by eauto; subst u. intros v Hv; destruct (Hin _ _ Hv) as [H'|[H'|[H'|H']]]; discriminate H'. intros u Hu v Hv; destruct (Hin3 _ _ Hz _ Hu _ Hv); discriminate. intros z Hz u Hu v Hv; destruct (Hin3 _ _ Hz _ Hu _ Hv); discriminate. intros z Hz; destruct (Hin _ _ Hz) as [H'|[H'|[H'|H']]]; discriminate H'. intros x Hx; assert (H' := Hin4 _ _ Hx _ Hx _ Hx _ Hx); subst x. destruct (Hin' _ _ Hx) as [H'|[H'|[H'|H']]]; discriminate. Qed.
imports: ZArith List String Bool syntax little axiom abstract_i