fact: Definition output_num_rewrites (n : Z) (m : Z) : Z := ((2^(n+1) - 1) * m)%Z.
imports: Coq.micromega.Lia Coq.ZArith.ZArith Coq.QArith.QArith Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Lists.List PerformanceExperiments.Harness