proposition: Lemma memMemCPOK : forall cp s, (forall e, InCP e cp -> S.mem e s = true) -> memCP cp s = true.
proof: Proof. apply memMemCPAuxOK. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets