proposition: Lemma l8_13_2 : forall A B C D X, A <> B -> C <> D -> Col X A B -> Col X C D -> (exists U, exists V :Tpoint, Col U A B /\ Col V C D /\ U<>X /\ V<>X /\ Per U X V) -> Perp_at X A B C D.
proof: Proof. intros. ex_and H3 U. ex_and H4 V. unfold Perp_at. repeat split;try assumption. intros. assert (Per V X U0). eapply l8_2. eapply l8_3. apply H7. assumption. eapply col3. apply H. Col. Col. Col. apply per_col with V. auto. apply l8_2. assumption. eapply col3. apply H0. Col. Col. Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR