proposition: Lemma col_3 : forall (COL : cartesianPower Tpoint 3) (DIFF : cartesianPower Tpoint 2), pred_conj col COL DIFF -> app diff DIFF -> app col COL.
proof: Proof. unfold pred_conj. unfold col. unfold diff. simpl in *. intros COL DIFF HCol HDiff. destruct HCol as [HCol1 [HCol2 HCol3]]. apply col3 with (fst DIFF) (snd DIFF); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch06_out_lines GeoCoq.Tactics.Coinc.tactics_axioms