proposition: Theorem inj_sub p q : (q < p)%positive -> to_nat (p - q) = to_nat p - to_nat q.
proof: Proof. intro H. apply Nat.add_cancel_r with (to_nat q). rewrite Nat.sub_add. - now rewrite <- inj_add, sub_add. - now apply Nat.lt_le_incl, inj_lt. Qed.
imports: BinPos PeanoNat