proposition: Lemma big_int_recr m n F : m <= n -> \big[op/idx]_(m <= i < n + 1 :> int) F i = op (\big[op/idx]_(m <= i < n :> int) F (i)) (F n).
proof: Proof. move=> hmn; rewrite (@big_cat_int n) ?ler_wpDr //=. rewrite big_addz2l (@big_ltz 0 1) // add0r (@big_geqz 1 1) // add0r. by rewrite Monoid.Theory.mulm1. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp