proposition: Lemma big_nat1_id n F : \big[op/x]_(n <= i < n.+1) F i = op (F n) x.
proof: Proof. by rewrite big_ltn // big_geq // mulm1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)