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