proposition: Lemma image_image_in : forall A B P P' M, P <> P'-> ReflectL P P' A B -> Col A B M -> Col P M P' -> ReflectL_at M P P' A B.
proof: Proof. intros. unfold ReflectL_at. split. split. assert(HH:=H0). unfold ReflectL in H0. spliter. ex_and H0 M'. induction H3. assert (Perp P M' A B). eapply perp_col. intro. subst P. apply l7_2 in H0. apply is_midpoint_id in H0. subst P'. apply perp_distinct in H3. spliter. absurde. apply perp_sym. apply perp_right_comm. apply H3. unfold Col. right; left. apply midpoint_bet. assumption. assert (M'=M). apply (l6_21 A B P P'); Col. induction (eq_dec_points A M'). subst M'. assert (~ Col A B P /\ Per P A B). eapply l8_16_1. apply col_trivial_3. apply col_trivial_2. apply perp_distinct in H3. spliter. auto. apply perp_sym. assumption. spliter. intro. apply H6. assumption. assert (~ Col A B P /\ Per P M' A). eapply l8_16_1. assumption. apply col_trivial_3. apply perp_sym. assumption. spliter. intro. apply H7. assumption. apply perp_distinct in H3. spliter. auto. subst M'. assumption. subst P'. absurde. assumption. assert (HH:=H0). unfold ReflectL in H0. spliter. induction H3. left. assumption. right. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop