proposition: Lemma eq_big_int_nat_cond m n F P : \big[op/idx]_(Posz m <= i < Posz n :> int | P i) F i = \big[op/idx]_(m <= i < n | P (Posz i)) F (Posz i).
proof: Proof. by rewrite /index_iotaz big_map. Qed.
imports: mathcomp(all_ssreflect all_algebra) extra_mathcomp