proposition: Lemma ex_sym : forall A B X, exists Y, (Perp A B X Y \/ X = Y) /\ (exists M, Col A B M /\ Midpoint M X Y).
proof: Proof. intros. induction (col_dec A B X). exists X. split. right. reflexivity. exists X. split. assumption. apply l7_3_2. assert (exists M, Col A B M /\ Perp A B X M). apply l8_18_existence. assumption. ex_and H0 M0. double X M0 Z. exists Z. split. left. apply perp_sym. eapply perp_col. intro. subst Z. apply l7_3 in H2. subst X. apply perp_distinct in H1. spliter. absurde. apply perp_sym. apply H1. unfold Col. left. apply midpoint_bet. assumption. exists M0. split. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop