comment to explain what happens in big_opM_singletons

theories/algebra/gmap.v

@@ -598,6 +598,11 @@ Qed.
 Lemma big_opM_singletons m :
   ([^op map] k ↦ x ∈ m, {[ k := x ]}) = m.
 Proof.
+  (* We are breaking the big_opM abstraction here. The reason is that [map_ind]
+     is too weak: we need an induction principle that visits all the keys in the
+     right order, namely the order in which they appear in map_to_list.  Here,
+     we achieve this by unfolding [big_opM] and doing induction over that list
+     instead. *)
   rewrite big_opM_eq /big_opM_def -{2}(list_to_map_to_list m).
   assert (NoDup (map_to_list m).*1) as Hnodup by apply NoDup_fst_map_to_list.
   revert Hnodup. induction (map_to_list m) as [|[k x] l IH]; csimpl; first done.