proposition: Lemma inj_sub n m : (m<=n)%N -> Z.of_N (n-m) = Z.of_N n - Z.of_N m.
proof: Proof. intros H. rewrite inj_sub_max. unfold N.le in H. rewrite N.compare_antisym, <- inj_compare, Z.compare_sub in H. destruct (Z.of_N n - Z.of_N m); trivial; now destruct H. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat