proposition: Lemma inj_pred n : (0<n)%nat -> Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n).
proof: Proof. rewrite nat_compare_lt, Nat2N.inj_compare. intros. now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat