proposition: Lemma unfold_reduce s c p : Associational.reduce s c p = prod_rect (fun _ => _) (fun lo hi => lo ++ Associational.mul c hi) (Associational.split s p).
proof: Proof. cbv [Associational.reduce]; edestruct Associational.split; reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround