proposition: Lemma ex_points_ang : forall a , Q_CongA a -> exists A, exists B, exists C, a A B C.
proof: Proof. intros. unfold Q_CongA in H. ex_and H A. ex_and H0 B. ex_and H C. assert(HH:= H1 A B C). destruct HH. exists A. exists B. exists C. apply H2. apply conga_refl; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch13_2_length