Axiom Int : Set.
Axiom Less : Int → Int → Prop.
Axiom Equal : Int → Int → Prop.
Axiom int_succ : ∀ x : Int, {y : Int | Less x y}.
Axiom int_null : Int.

Axiom equal_dec : ∀ x y : Int, {Equal x y} + {¬ Equal x y}.
Axiom less_dec : ∀ x y : Int, {Less x y} + {¬ Less x y}.

Axiom
  notequal_notless_greater :
    ∀ x y : Int, ¬ Equal x y → ¬ Less x y → Less y x.

Axiom less_trans : ∀ x y z : Int, Less x y → Less y z → Less x z.
Axiom equal_less_less : ∀ x y z : Int, Equal x y → Less y z → Less x z.
Axiom less_equal_less : ∀ x y z : Int, Less x y → Equal y z → Less x z.
Axiom equal_sym : ∀ x y : Int, Equal x y → Equal y x.
Axiom equal_trans : ∀ x y z : Int, Equal x y → Equal y z → Equal x z.
Axiom equal_refl : ∀ x : Int, Equal x x.
Axiom equal_eq : ∀ x y : Int, Equal x y → x = y.

Axiom less_irrefl : ∀ x : Int, Less x x → False.

Lemma equal_dec_refl :
 ∀ (i : Int) (A : Set) (a b : A),
 match equal_dec i i with
 | left _ ⇒ a
 | right _ ⇒ b
 end = a.
intros i A a b.
elim (equal_dec i i).
intros; trivial.
intros notequal; elimtype False; apply notequal.
apply equal_refl.
Qed.

Inductive max_int_spec (i0 i1 : Int) : Set :=
    Max_Int_Intro :
      ∀ j : Int,
      Less i0 j ∨ Equal i0 j →
      Less i1 j ∨ Equal i1 j → max_int_spec i0 i1.

Lemma max_int : ∀ i0 i1 : Int, max_int_spec i0 i1.
intros i0 i1.
elim (equal_dec i0 i1).
intros eq_i0_i1.
∃ i0.
right.
apply equal_refl.
right.
apply equal_sym; assumption.

intros not_eq_i0_i1.
elim (less_dec i0 i1).
intros less_i0_i1.
∃ i1.
left; assumption.
right.
apply equal_refl.

intros ge_i0_i1.
∃ i0.
right.
apply equal_refl.
left.
apply notequal_notless_greater; assumption.
Qed.