proposition: Lemma STadd_iff : forall (s : STt) (x y : STelt), STmem y (STadd x s) = true <-> (eqST x y \/ STmem y s = true).
proof: Proof. intros; simpl; elim (eqST_dec x y);intro;intuition. Qed.
imports: MSets Arith NArith Notations Sorting Coq.Program.Equality GeoCoq.Tactics.Coinc.tactics_axioms