proposition: Lemma is_image_spec_col_cong : forall A B P P' X, ReflectL P P' A B -> Col A B X -> Cong P X P' X.
proof: Proof. intros. unfold ReflectL in *. spliter. ex_and H M0. induction H1. assert (HH:= H1). apply perp_distinct in HH. spliter. induction (eq_dec_points M0 X). subst X. unfold Midpoint in *. spliter. Cong. assert (Perp M0 X P' P) by (eauto using perp_col2). assert(~ Col A B P /\ Per P M0 X). eapply l8_16_1. assumption. assumption. auto. apply perp_sym. eapply perp_col. intro. subst P. apply l7_2 in H. apply is_midpoint_id in H. subst P'. absurde. apply perp_left_comm. apply perp_sym. apply H1; eapply perp_left_comm. unfold Col. right; left. apply midpoint_bet. assumption. spliter. eapply l8_2 in H8. unfold Per in H8. ex_and H8 P0. assert (P0 = P'). eapply symmetric_point_uniqueness. apply H8. apply l7_2. assumption. subst P0. Cong. subst. Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop