proposition: Lemma id' n : N.to_nat (N.of_nat n) = n.
proof: Proof. induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance