proposition: Lemma inj_sub n m : 0<=m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N.
proof: Proof. destruct n as [|n|n], m as [|m|m]; trivial; try (now destruct 1). intros _. simpl. rewrite Z.pos_sub_spec, Pos.compare_sub_mask. unfold Pos.sub. now destruct (Pos.sub_mask n m). Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat