proposition: Lemma cop_3 : forall (COP : cartesianPower Tpoint 4) (NOT_COL : cartesianPower Tpoint 3), pred_conj cop COP NOT_COL -> app not_col NOT_COL -> app cop COP.
proof: Proof. unfold pred_conj. unfold cop. unfold not_col. simpl in *. intros COP NOT_COL HCop HNot_Col. destruct HCop as [HCop1 [HCop2 [HCop3 HCop4]]]. apply coplanar_pseudo_trans with (fst NOT_COL) (fst (snd NOT_COL)) (snd (snd NOT_COL)); Cop. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tactics.Coinc.tactics_axioms