proposition: Lemma big_ord_recl n F : \big[op/idx]_(i < n.+1) F i = op (F ord0) (\big[op/idx]_(i < n) F (@lift n.+1 ord0 i)).
proof: Proof. pose G i := F (inord i); have eqFG i: F i = G i by rewrite /G inord_val. under eq_bigr do rewrite eqFG; under [in RHS]eq_bigr do rewrite eqFG. by rewrite -(big_mkord _ (fun _ => _) G) eqFG big_ltn // big_add1 /= big_mkord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)