proposition: Lemma DnsCache_addE_is_plus1 : forall n (cache: @Cache.CacheEncode DnsMap.cache), addE_n n cache = {| DnsMap.eMap := DnsMap.eMap cache; DnsMap.dMap := DnsMap.dMap cache; DnsMap.offs := DnsMap.offs cache + N.of_nat n |}.
proof: Proof. Opaque N.of_nat. induction n; destruct cache; simpl in *. + rewrite N.add_0_r; reflexivity. + rewrite IHn; simpl in *. rewrite <- N.add_assoc, N.add_1_l, Nat2N.inj_succ; reflexivity. Transparent N.of_nat. Qed.
imports: CertifiedExtraction.Benchmarks.MicrobenchmarksSetup CertifiedExtraction.Extraction.BinEncoders.BinEncoders Coq.Program.Program