proposition: Lemma to_of_nat x y : of_nat x = Some y -> to_nat y = x.
proof: Proof. do 256 try destruct x as [|x]; cbv [of_nat]; intro. all: repeat match goal with | _ => reflexivity | _ => progress subst | [ H : Some ?a = Some ?b |- _ ] => assert (a = b) by refine match H with eq_refl => eq_refl end; clear H | [ H : None = Some _ |- _ ] => solve [ inversion H ] end. Qed.
imports: Coq.Arith.EqNat Coq.NArith.BinNat Coq.NArith.Nnat Coq.Init.Byte