proposition: Lemma big_nat_recl n m F : m <= n -> \big[op/idx]_(m <= i < n.+1) F i = op (F m) (\big[op/idx]_(m <= i < n) F i.+1).
proof: Proof. by move=> lemn; rewrite big_ltn // big_add1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)