proposition: Lemma big_geqz m n (P : pred int) F : m >= n -> \big[op/idx]_(m <= i < n :> int | P i) F i = idx.
proof: Proof. case: m => m; case: n => // n; rewrite /index_iotaz ?big_nil //. by rewrite lez_nat /index_iota; move/eqnP->; rewrite big_nil. rewrite ![in _ <= _]NegzE lerN2 lez_nat /index_iota; move/eqnP->. by rewrite big_nil. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp