proposition: Lemma natmap_lookup_singleton_raw_ne {A} (i j : nat) (x : A) : i ≠ j → mjoin (natmap_singleton_raw i x !! j) = None.
proof: Proof. revert j; induction i; intros [|?]; simpl; auto with congruence. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)