proposition: Lemma inj_sub n m : 0<=m<=n -> Z.abs_N (n-m) = (Z.abs_N n - Z.abs_N m)%N.
proof: Proof. intros (Hn,H). rewrite !abs_N_nonneg; trivial. - now apply Z2N.inj_sub. - Z.order. - now apply Z.le_0_sub. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat