proposition: Lemma ss_ok_inter_ok1 : forall ss interp s1 s2 x (p : cartesianPower positive 1), ss_ok ss interp -> SS.In s1 ss -> pick_variety_aux (S.inter s1 s2) x = true -> S.mem p s1 = true -> app_1_n coinc (interp_CP p interp) (interp_CP x interp).
proof: Proof. intros ss interp s1 s2 x p HSSOK HIn HInter Hmem. apply app_app_1_n with (consHeadCP (interp_CP p interp) (interp_CP x interp)); try (simpl; reflexivity). assert (Hmemcp : memCPAux n x s1 = true) by (apply pick_variety_aux_memCPAux1 with s2; assumption). unfold ss_ok in HSSOK. rewrite consHdInterpOK. apply SSWEqP.MP.Dec.F.mem_1 in HIn. apply HSSOK with s1; try assumption. apply memCPConsHd; assumption. Qed.
imports: Recdef NArith Sorting GeoCoq.Tactics.Coinc.Permutations GeoCoq.Utils.general_tactics GeoCoq.Utils.sets