proposition: Lemma inj_sub a a' : N.to_nat (a - a') = N.to_nat a - N.to_nat a'.
proof: Proof. destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial. destruct (Pos.compare_spec a a') as [H|H|H]. - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag. - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl. - destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq). simpl; symmetry; apply Nat.add_sub_eq_l. now rewrite <- Hq, Pos2Nat.inj_add. Qed.
imports: BinPos BinNat PeanoNat Pnat