proposition: Lemma memMemCPAuxOK : forall m cp s, (forall e, InCP e cp -> S.mem e s = true) -> memCPAux m cp s = true.
proof: Proof. induction m. unfold memCPAux. simpl. intros cp s H. rewrite andb_true_iff. assert (HIn1 : InCP (fst cp) cp) by (unfold InCP; simpl; auto). assert (HIn2 : InCP (snd cp) cp) by (unfold InCP; simpl; auto). split; apply H; assumption. intros cp s H. rewrite memCPAuxHdTl. rewrite andb_true_iff. assert (HIn : InCP (fst cp) cp) by (unfold InCP; simpl; auto). split; try (apply H; assumption); clear HIn. apply IHm. intros e HIn. apply H. apply InCPOK. right. assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets