proposition: Lemma fold_right_cons {A B} (f : B -> A -> A) (a : A) (b : B) (bs : list B) : fold_right f a (b :: bs) = f b (fold_right f a bs).
proof: Proof. 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