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