proposition: Lemma eq_points_coordinates : forall O E S U1 U2 P1 X1 Y1 P2 X2 Y2, Cd O E S U1 U2 P1 X1 Y1 -> Cd O E S U1 U2 P2 X2 Y2 -> (P1 = P2 <-> (X1 = X2 /\ Y1 = Y2)).
proof: Proof. intros O E S U1 U2 P1 X1 Y1 P2 X2 Y2 HCd1 HCd2. split; intro; spliter; treat_equalities. { destruct HCd1 as [HCs [H [[PX HPX1] [PY HPY1]]]]; clear H. destruct HCd2 as [H [H' [[PX2 HPX2] [PY2 HPY2]]]]; clear H; clear H'. assert (PX = PX2) by (spliter; apply projp_id with P1 S U1; auto); treat_equalities; assert (PY = PY2) by (spliter; apply projp_id with P1 S U2; auto); treat_equalities. destruct HPX1 as [H HCong1]; assert (H' : Col PX S U1) by (destruct H as [H' H]; induction H; spliter; treat_equalities; Col). clear H; assert (HCol1 : Col O E X1) by (apply l4_13 with S U1 PX; Col; Cong). clear H'; destruct HPX2 as [H HCong3]; clear H. destruct HPY1 as [H HCong2]; assert (H' : Col PY S U2) by (destruct H as [H' H]; induction H; spliter; treat_equalities; Col). clear H; assert (HCol2 : Col O E Y1) by (apply l4_13 with S U2 PY; Col; Cong). clear H'; destruct HPY2 as [H HCong4]; clear H. unfold Cs in HCs; spliter. split; apply l4_18 with O E; Col; unfold Cong_3 in *; spliter; eapply cong_transitivity; eCong. } { destruct HCd1 as [HCs [H [[PX HPX1] [PY HPY1]]]]; clear H. destruct HCd2 as [H [H' [[PX2 HPX2] [PY2 HPY2]]]]; clear H; clear H'. assert (PX = PX2); treat_equalities. { destruct HPX1 as [[H HElim] H0]; unfold Cs in HCs; unfold Cong_3 in *; spliter; assert_diffs; apply l4_18 with S U1; auto. induction HElim; spliter; treat_equalities; Col. apply cong_transitivity with O X1; Cong. apply cong_transitivity with E X1; Cong. } assert (PY = PY2); treat_equalities. { destruct HPY1 as [[H HElim] H0]; unfold Cs in HCs; unfold Cong_3 in *; spliter; assert_diffs; apply l4_18 with S U2; auto. induction HElim; spliter; treat_equalities; Col. apply cong_transitivity with O Y1; Cong. apply cong_transitivity with E Y1; Cong. } destruct HPX1 as [HProjp1 H]; clear H; destruct HPX2 as [HProjp2 H]; clear H; destruct HPY1 as [HProjp3 H]; clear H; destruct HPY2 as [HProjp4 H]; clear H. assert (HCol1 : Col PX P1 P2) by (apply projp2_col with S U1; auto). assert (HCol2 : Col PY P1 P2) by (apply projp2_col with S U2; auto). elim (eq_dec_points P1 P2); intro HP1P2; treat_equalities; auto; exfalso. assert (HPar : Par S U1 S U2). { elim (eq_dec_points P1 PX); intro HP1PX; elim (eq_dec_points P1 PY); intro HP1PY; treat_equalities. { destruct HProjp2 as [H H1]; clear H; elim H1; clear H1; intro H1; [destruct H1 as [H1 HPerp1]|spliter; intuition]. destruct HProjp4 as [H H2]; clear H; elim H2; clear H2; intro H2; [destruct H2 as [H2 HPerp2]|spliter; intuition]. apply l12_9_2D with P2 P1; Perp. } { destruct HProjp2 as [H H1]; clear H; elim H1; clear H1; intro H1; [destruct H1 as [H1 HPerp1]|spliter; intuition]. destruct HProjp3 as [H H2]; clear H; elim H2; clear H2; intro H2; [destruct H2 as [H2 HPerp2]|spliter; intuition]. apply l12_9_2D with P2 P1; Perp. apply perp_col0 with P1 PY; Perp; Col. } { destruct HProjp1 as [H H1]; clear H; elim H1; clear H1; intro H1; [destruct H1 as [H1 HPerp1]|spliter; intuition]. destruct HProjp4 as [H H2]; clear H; elim H2; clear H2; intro H2; [destruct H2 as [H2 HPerp2]|spliter; intuition]. apply l12_9_2D with P2 P1; Perp. apply perp_col0 with P1 PX; Perp; Col. } { destruct HProjp1 as [H H1]; clear H; elim H1; clear H1; intro H1; [destruct H1 as [H1 HPerp1]|spliter; intuition]. destruct HProjp3 as [H H2]; clear H; elim H2; clear H2; intro H2; [destruct H2 as [H2 HPerp2]|spliter; intuition]. apply l12_9_2D with P2 P1; [apply perp_col0 with P1 PX|apply perp_col0 with P1 PY];Perp; Col. } } assert (HFalse : ~ ~ Col U1 S U2). { intro HF; apply HF; elim HPar; clear HPar; intro HPar; spliter; Col. exfalso; apply HPar; exists S; Col. } unfold Cs in HCs; spliter; assert_diffs; apply HFalse; apply per_not_col; Col. } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths