proposition: Theorem falling_seq_correct (d : Z) (p : Z) (n k : nat) : k <= n -> nth d (falling_seq p n) k = \big[Z.mul/1%Z]_(0 <= i < k) (p - Z.of_nat i)%Z.
proof: Proof. elim: k => [|k IHk] Hkn; first by rewrite rec1up_co0 big_mkord big_ord0. move/(_ (ltnW Hkn)) in IHk. move: IHk. rewrite /falling_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 /falling_rec. rewrite big_nat_recr //=. congr Z.mul. zify; ring. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp