proposition: Lemma l8_16_1 : forall A B C U X, Col A B X -> Col A B U -> Perp A B C X -> ~ Col A B C /\ Per C X U.
proof: Proof. intros. destruct (eq_dec_points U X). subst X. split. destruct (perp_not_col2 A B C U); auto. apply l8_5. split. intro. assert (Perp_at X A B C X). eapply l8_15_1. assumption. assumption. assert (X = U). eapply l8_14_2_1b. apply H4. Col. eapply col3 with A B;Col. apply perp_distinct in H1; spliter; auto. intuition. apply l8_14_2_1b_bis with C X U X; Col. assert (Col A X U). eapply (col3 A B);Col. apply perp_distinct in H1; spliter; auto. eapply perp_col0 with A B;Col. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR