Library Coq.Arith.Peano_dec


Require Import Decidable.




Open Local Scope nat_scope.




Implicit Types m n x y : nat.




Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}.

Proof.

induction n.

auto.

left; exists n; auto.

Defined.




Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}.

Proof.

induction n; induction m; auto.

elim (IHn m); auto.

Defined.




Hint Resolve O_or_S eq_nat_dec: arith.




Theorem dec_eq_nat : forall n m, decidable (n = m).

intros x y; unfold decidable in |- *; elim (eq_nat_dec x y); auto with arith.

Defined.

Index

This page has been generated by coqdoc