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.