proposition: Lemma big_map_id J (h : J -> R) r (P : pred R) : \big[op/idx]_(i <- map h r | P i) i = \big[op/idx]_(j <- r | P (h j)) h j.
proof: Proof. exact: big_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)