fact: Fixpoint fac_help (n : nat) (m c : A) : A := match n with | O => c | S n => (m + naturals_to_semiring nat A n) * fac_help n m c end.
imports: Coq.setoid_ring.Ring Coq.Arith.Factorial MathClasses.misc.workaround_tactics MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.interfaces.naturals MathClasses.interfaces.integers MathClasses.theory.nat_pow MathClasses.theory.int_pow MathClasses.theory.streams