proposition: Lemma memCPAuxHdTl : forall m cp s, memCPAux (S m) cp s = S.mem (fst cp) s && memCPAux m (tailCP cp) s.
proof: Proof. induction m; unfold memCPAux; unfold nat_rect; reflexivity. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets