proposition: Lemma remove_in m x y `{!Ok m} : y ∈ (remove x m) <-> y ∈ m /\ ~ y==x.
proof: Proof. unfold remove. now autorew. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)