fact: Definition Z_prod_count_exact (min max : Z * Z) : N := (let min := fst min * snd min in let max := fst max * snd max in Z.to_N (∑_{i=1}^{max} (1 + Qfloor (max/i) + Qceiling (min/i))))%Z.
imports: Coq.Strings.String Coq.Structures.Orders Coq.micromega.Lia Coq.Bool.Bool Coq.Sorting.Mergesort Coq.QArith.QArith Coq.QArith.Qround Coq.QArith.Qabs Coq.QArith.Qminmax Coq.NArith.NArith Coq.ZArith.ZArith Coq.Arith.Arith Coq.Lists.List PerformanceExperiments.LetIn