proposition: Lemma eqdec : forall n m : nat, n = m \/ n <> m.
proof: Proof. simple induction n. intro. case m. left. reflexivity. right. discriminate. intros. case m. right. discriminate. intro m0. elim (H m0). left. rewrite H0. reflexivity. right. intro. apply H0. inversion H1. reflexivity. Qed.
imports: Arith ZArith EqNat