proposition: Theorem fold_add_const_mult : forall (A : Type)(ls : list A)(c : nat) init, (fold_left (fun acc _ => acc + c) ls init = (length ls) * c + init)%nat.
proof: Proof. induction ls; intuition; simpl in *. rewrite IHls. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation