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