proposition: Lemma alter_strict_mono {A} f (m1 m2 : M A) i : m1 ⊂ m2 → alter f i m1 ⊂ alter f i m2.
proof: Proof. rewrite !map_subset_alt. intros [? (j&?&?)]; split; auto using alter_mono. exists j. by rewrite lookup_alter_None, lookup_alter_is_Some. Qed.
imports: Coq(Permutation) stdpp(options)