proposition: Lemma to_of_nat_iff x y : of_nat x = Some y <-> to_nat y = x.
proof: Proof. split; intro; subst; (apply of_to_nat || apply to_of_nat); assumption. Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte