proposition: Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a).
proof: Proof. destruct a as [|[p|p| ]]; trivial. - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double. - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double. Qed.
imports: BinPos BinNat PeanoNat Pnat