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