proposition: Theorem inj_pred : forall n : nat, n <> 0 -> Z_of_nat (pred n) = Z.pred (Z_of_nat n).
proof: Proof. intros n; case n; auto. intros H'; contradict H'; auto. intros n0 H'; rewrite inj_S; rewrite <- Zpred_succ; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz