proposition: Lemma inj_compare p q : (p ?= q)%positive = (to_nat p ?= to_nat q).
proof: Proof. revert q. induction p as [ |p IH] using peano_ind; intros q. - destruct (succ_pred_or q) as [Hq|Hq]; [now subst|]. rewrite <- Hq, lt_1_succ, inj_succ, inj_1, Nat.compare_succ. symmetry. apply Nat.compare_lt_iff, is_pos. - destruct (succ_pred_or q) as [Hq|Hq]; [subst|]. + rewrite compare_antisym, lt_1_succ, inj_succ. simpl. symmetry. apply Nat.compare_gt_iff, is_pos. + now rewrite <- Hq, 2 inj_succ, compare_succ_succ, IH. Qed.
imports: BinPos PeanoNat