proposition: Lemma collect_coincs : forall cp ss interp, app coinc (interp_CP cp interp) -> ss_ok ss interp -> ss_ok (SS.add (CPToSS cp) ss) interp.
proof: Proof. intros cp ss interp HCoapp HSS. unfold ss_ok. intros s Hs. intros cp' Hmem. apply SSWEqP.MP.Dec.F.mem_2 in Hs. apply SSWEqP.MP.Dec.F.add_iff in Hs. elim Hs; clear Hs; intro Hs. assert (HDup := NoDup_dec (CPToList cp') Pos.eq_dec). elim HDup; clear HDup; intro HDup. assert (Hincl := CPToSSOK cp cp' s Hs Hmem). assert (Hlength : length (CPToList cp') = length (CPToList cp)) by (do 2 (rewrite <- lengthOfCPToList); reflexivity). assert (HPerm := NoDupOK (CPToList cp') (CPToList cp) Hincl Hlength HDup). apply Permutation.Permutation_map with positive COINCpoint interp (CPToList cp') (CPToList cp) in HPerm. do 2 (rewrite <- interp_CPOK in HPerm); clear HDup; clear Hincl; clear Hlength. apply Permutation.Permutation_sym in HPerm. apply PermCoincOK with (interp_CP cp interp); assumption. apply CoappDup; assumption. unfold ss_ok in HSS. apply HSS with s; try assumption. apply SSWEqP.MP.Dec.F.mem_1; assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets