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