proposition: Lemma inj_sub n m : (m<=n)%nat -> Z.of_nat (n-m) = Z.of_nat n - Z.of_nat m.
proof: Proof. rewrite nat_compare_le, Nat2N.inj_compare. intros. now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat