proposition: Lemma inj_pred n : 0<n -> Z.abs_N (Z.pred n) = N.pred (Z.abs_N n).
proof: Proof. intros. rewrite !abs_N_nonneg. - now apply Z2N.inj_pred. - Z.order. - apply Z.lt_succ_r. now rewrite Z.succ_pred. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat