proposition: Lemma add_rem_neq a b P : a <> b -> add a (rem b P) [=] rem b (add a P).
proof: Proof. intro nab. split. fo. subst. hyp. fo. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(LogicUtil RelUtil FunUtil ListUtil NatUtil ClassicUtil BoundNat)