proposition: Theorem fact_seq_correct (d : Z) (n k : nat) : k <= n -> nth d (fact_seq n) k = Z.of_nat (fact k).
proof: Proof. elim: k => [|k IHk] Hkn; first by rewrite rec1up_co0. move/(_ (ltnW Hkn)) in IHk. move: IHk. rewrite /fact_seq. rewrite (@nth_rec1up_indep _ _ _ d d _ k); try exact: ltnW || exact: leqnn. move => IHk. rewrite (@nth_rec1up_indep _ _ _ d d _ k.+1) //. rewrite nth_rec1upS IHk /fact_rec. rewrite fact_simpl. zify; ring. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp