proposition: Lemma big_int_recl n F : 0 < n + 1 -> \big[op/idx]_(0 <= i < n + 1 :> int) F i = op (F 0) (\big[op/idx]_(0 <= i < n :> int) F (i + 1)).
proof: Proof. by move=> pSn; rewrite big_ltz // add0r big_addz2r. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp