proposition: Lemma l8_16_2 : forall A B C U X, Col A B X -> Col A B U -> U<>X -> ~ Col A B C -> Per C X U -> Perp A B C X.
proof: Proof. intros. assert (C <> X). intro. subst X. apply H2. assumption. unfold Perp. exists X. eapply l8_13_2. assert_diffs; auto. assumption. Col. Col. exists U. exists C. repeat split; Col. apply l8_2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR