proposition: Lemma inj_compare a a' : (a ?= a')%N = (N.to_nat a ?= N.to_nat a').
proof: Proof. destruct a as [|p], a' as [|p']; simpl; trivial. - now destruct (Pos2Nat.is_succ p') as (n,->). - now destruct (Pos2Nat.is_succ p) as (n,->). - apply Pos2Nat.inj_compare. Qed.
imports: BinPos BinNat PeanoNat Pnat