proposition: Lemma exists_cong_per : forall A B X Y, exists C, Per A B C /\ Cong B C X Y.
proof: Proof. intros. destruct (eq_dec_points A B). subst. destruct (segment_construction X B X Y). exists x;split;spliter;Perp. destruct (not_col_exists A B H) as [P HP]. destruct (eq_dec_points X Y). subst;exists B;split;[Perp|Cong]. destruct (ex_per_cong A B B P X Y); Col. spliter. exists x;split;[Perp|Cong]. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop