proposition: Lemma inj_sub n m : 0<=m<=n -> Z.abs_nat (n-m) = (Z.abs_nat n - Z.abs_nat m)%nat.
proof: Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_sub, N2Nat.inj_sub. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat