proposition: Lemma perp_exists : forall O A B, A <> B -> exists X, Perp O X A B.
proof: Proof. intros. induction(col_dec A B O). destruct (diff_col_ex3 A B O H0) as [C]. spliter. destruct (l8_21 O C O H3) as [P [T]]. spliter. exists P. apply perp_comm. apply perp_sym. apply (perp_col2 O C); ColR. destruct (l8_18_existence A B O H0) as [X []]. exists X. apply perp_sym. apply H2. Qed.
imports: GeoCoq.Tarski_dev.Ch07_midpoint GeoCoq.Tactics.Coinc.ColR