proposition: Lemma l10_2_existence_spec : forall A B P, exists P', ReflectL P' P A B.
proof: Proof. intros. induction (col_dec A B P). unfold ReflectL. exists P. split. exists P. split. apply l7_3_2. assumption. right. reflexivity. assert (exists X, Col A B X /\ Perp A B P X). eapply l8_18_existence. assumption. ex_and H0 X. double P X P'. exists P'. unfold ReflectL. split. exists X. split; assumption. left. apply perp_sym. eapply perp_col. intro. subst P'. 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. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop