proposition: Lemma Str_nth_factorials_help (n : nat) (m c : A) : Str_nth n (factorials_help m c) = fac_help n m c.
proof: Proof. revert m c. induction n using peano_naturals.nat_induction; intros m c; unfold Str_nth in *; simpl. ring. rewrite IHn. clear IHn. induction n using peano_naturals.nat_induction; simpl. rewrite rings.preserves_0. now ring. rewrite IHn, rings.preserves_plus, rings.preserves_1. now ring. Qed.
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