NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library EqNat_ext

Require Import EqNat.
Export EqNat.

Lemma beq_nat_sym : forall a b, beq_nat a b = beq_nat b a.

Lemma beq_nat_classic : forall a b, beq_nat a b = true \/ beq_nat a b = false.

Lemma neq_beq_nat : forall n m, n <> m -> beq_nat n m = false.