proposition: Lemma inj_sub (n m : nat) : m<>0 -> Pos.of_nat (n-m) = (Pos.of_nat n - Pos.of_nat m)%positive.
proof: Proof. intros Hm. apply Pos2Nat.inj. rewrite Pos2Nat.inj_sub_max. rewrite (id m) by trivial. rewrite !id_max. destruct n, m; trivial. Qed.
imports: BinPos PeanoNat