fact: Fixpoint func_iter n A B (F:(A->B)->(A->B)) (f:A->B) (x:A) : B := match n with | O => f x | S n' => F (func_iter n' F f) x end.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)