proposition: Lemma test_col_ok : forall ss sp interp p1 p2 p3, ss_ok ss interp -> sp_ok sp interp -> test_col ss sp p1 p2 p3 = true -> CTCol (interp p1) (interp p2) (interp p3).
proof: Proof. intros ss sp interp p1 p2 p3 HSS HSP HTC. unfold test_col in *. assert (HSS2 : ss_ok (identify_lines ss sp) interp) by (apply identify_lines_ok; assumption). unfold ss_ok in HSS2. apply SSWEqP.MP.Dec.F.exists_2 in HTC. unfold SS.Exists in HTC. destruct HTC as [s [HIn Hmem]]. apply HSS2 with s. apply SSWEqP.MP.Dec.F.mem_1. assumption. assumption. intros x y Hxy. assert (HmemEq : forall p, S.mem p x = S.mem p y) by (intro; apply SWP.Dec.F.mem_m; auto). do 3 (rewrite HmemEq); reflexivity. Qed.
imports: Recdef NArith GeoCoq.Utils.sets