proposition: Lemma inject_nat_convert : forall p : positive, Z_of_nat (nat_of_P p) = BinInt.Zpos p.
proof: Proof. intros. elim (ZL4 p); intros. rewrite H. simpl in |- *. apply (f_equal BinInt.Zpos). apply nat_of_P_inj. rewrite H. apply nat_of_P_o_P_of_succ_nat_eq_succ. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid