fact: Definition repeat_reduce (n : nat) (s:Z) (c:list _) (p:list _) : list (Z * Z) := nat_rect _ (fun p => p) (fun n' repeat_reduce_n' p => let lo_hi := split s p in if (length (snd lo_hi) =? 0)%nat then p else let p := fst lo_hi ++ mul c (snd lo_hi) in repeat_reduce_n' p) n p.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround