proposition: Lemma ex_point_lg : forall l A, Q_Cong l -> exists B, l A B.
proof: Proof. intros. induction(lg_null_dec l). exists A. apply lg_null_instance. auto. assert(HH:= H). unfold Q_Cong in HH. ex_and HH X. ex_and H1 Y. assert(HH:= another_point A). ex_and HH P. assert(HP:= H2 X Y). destruct HP. assert(l X Y). apply H3. apply cong_reflexivity. assert(X <> Y). intro. subst Y. apply H0. unfold Q_Cong_Null. split. auto. exists X. auto. assert(HH:= segment_construction_3 A P X Y H1 H6). ex_and HH B. exists B. assert(HH:= H2 A B). destruct HH. apply H9. Cong. auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_1