proposition: Lemma big_nat_leq_idx : forall (R : Type) (idx : R) (op : Monoid.law idx) (m n : nat) (F : nat -> R), n <= m -> (forall i : nat, n <= i < m -> F i = idx) -> \big[op/idx]_(0 <= i < n) F i = \big[op/idx]_(0 <= i < m) F i.
proof: Proof. move=> R idx op m n F Hmn H. rewrite [RHS](big_cat_nat _ (n := n)) //. rewrite [in X in _ = op _ X]big_nat_cond. rewrite [in X in _ = op _ X]big1 ?Monoid.mulm1 //. move=> i; rewrite andbT; move=> *; exact: H. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2