Library misc
Require Import Arith.
Theorem S_n_nbeq_n:
forall n,
beq_nat (S n) n = false.
Proof.
intro.
induction n.
simpl.
reflexivity.
assert (H_aux:
beq_nat (S (S n)) (S n) = beq_nat (S n) n).
simpl.
reflexivity.
rewrite H_aux; clear H_aux.
exact IHn.
Qed.
Require Import ZArith.
Remark Zeq_impl_nat_eq:
forall n m: nat,
(Z_of_nat n = Z_of_nat m)%Z -> (n = m)%nat.
Proof.
intros.
omega.
Qed.