proposition: Lemma inj_pred n : (0<n)%N -> Z.of_N (N.pred n) = Z.pred (Z.of_N n).
proof: Proof. intros H. unfold Z.pred. rewrite N.pred_sub, inj_sub; trivial. now apply N.le_succ_l in H. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat