proposition: Lemma image_id : forall A B T T', A<>B -> Col A B T -> Reflect T T' A B -> T = T'.
proof: Proof. intros. rewrite is_image_is_image_spec in H1 by apply H. unfold ReflectL in H1. spliter. ex_and H1 X. induction H2. assert (A <> B /\ T' <> T). apply perp_distinct in H2. spliter. split; assumption. spliter. induction (eq_dec_points A X). subst X. assert (Perp A B T' A). apply perp_sym. eapply perp_col. intro. subst T'. apply is_midpoint_id in H1. subst A. absurde. apply perp_sym. apply H2. unfold Col. right; left. apply midpoint_bet. apply l7_2. assumption. assert (~ Col A T' B). apply perp_not_col. apply perp_comm. apply perp_sym. assumption. assert (A = T). apply l6_21 with A T' B T; Col. intro; treat_equalities; Col. subst A. apply l7_2 in H1. apply is_midpoint_id in H1. subst T'. absurde. induction (eq_dec_points B X). subst X. assert (Perp A B T' B). apply perp_sym. eapply perp_col. intro. subst T'. apply is_midpoint_id in H1. subst B. absurde. apply perp_sym. apply H2. unfold Col. right; left. apply midpoint_bet. apply l7_2. assumption. assert (~ Col B T' A). apply perp_not_col. apply perp_left_comm. apply perp_sym. assumption. assert (B = T). eapply l6_21. apply H8. apply H4. apply col_trivial_3. unfold Col. right; right. apply midpoint_bet. apply l7_2. apply H1. apply col_trivial_2. assumption. subst B. apply l7_2 in H1. apply is_midpoint_id in H1. subst T'. absurde. assert (Col A X T) by ColR. assert (Perp A B T' X). apply perp_sym. eapply perp_col. intro. subst T'. apply is_midpoint_id in H1. subst X. absurde. apply perp_sym. apply H2. assert_cols. Col. assert (~ Col X T' A). apply perp_not_col. apply perp_left_comm. apply perp_sym. eapply perp_col. assumption. apply H9. assumption. assert (X = T). eapply l6_21. apply H10. apply H6. apply col_trivial_3. unfold Col. right; right. apply midpoint_bet. apply l7_2. apply H1. apply col_trivial_2. assumption. subst X. apply l7_2 in H1. apply is_midpoint_id in H1. subst T'. absurde. subst T'. reflexivity. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane GeoCoq.Tarski_dev.Tactics.CoincR_for_cop