proposition: Lemma inj_succ n : 0<=n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n).
proof: Proof. intros. rewrite !abs_N_nonneg; trivial. - now apply Z2N.inj_succ. - now apply Z.le_le_succ_r. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat