fact: Definition iter1 (A : Type) (op : operation A) (f : nat -> A) := fix s n := match n with | O => f O | S n' => op (f n) (s n') end.
imports: Type_class_definition Type_class_instance Coq.Relations.Relation_Definitions Lia Arith Nbinomial Setoid