proposition: Lemma square_distance_formula_aux : forall O E E' S U1 U2 P PX PY Q QX PXQX, Cd O E S U1 U2 P PX PY -> Cd O E S U1 U2 Q QX PY -> P <> Q -> ~ Col O E E' -> Col O E PX -> Col O E QX -> Col O E PY -> Cs O E S U1 U2 -> Length O E E' PX QX PXQX -> Length O E E' Q P PXQX.
proof: Proof. intros O E E' S U1 U2 P PX PY Q QX PXQX. intros HCd1 HCd2 HDiff HNC HCol1 HCol2 HCol3 HCs HPXQX. apply length_eq_cong_2 with PX QX; auto; clear HPXQX. destruct HCd1 as [H [H' [HPX' HPY']]]; clear H; clear H'. destruct HPX' as [PX' [HProjp1 HCong1]]; destruct HPY' as [PY' [HProjp2 HCong2]]. destruct HCd2 as [H [H' [HQX' HQY']]]; clear H; clear H'. destruct HQX' as [QX' [HProjp3 HCong3]]; destruct HQY' as [QY' [HProjp4 HCong4]]. assert (PY' = QY') by (assert_diffs; apply col_cong_3_cong_3_eq with O E PY S U2; auto). treat_equalities; assert (HPerp1 : Perp P Q S U2) by (apply projp_projp_perp with PY'; auto). assert (HPerp2 : Perp U1 S S U2) by (unfold Cs in HCs; spliter; assert_diffs; apply per_perp; Perp). destruct HProjp1 as [H H1]; clear H; destruct HProjp3 as [H H2]; clear H. elim H1; clear H1; intro H1; elim H2; clear H2; intro H2; destruct H1 as [HCol5 HPerp3]; destruct H2 as [HCol6 HPerp4]; treat_equalities. { elim (eq_dec_points S PX'); intro HDiff1; elim (eq_dec_points S QX'); intro HDiff2; treat_equalities. { exfalso; unfold Cong_3 in *; spliter; treat_equalities. assert (HPar1 : Par P Q S U1) by (apply l12_9_2D with S U2; Perp). assert (HPar2 : Par P S Q S) by (apply l12_9_2D with S U1; Perp). elim HPar2; clear HPar2; intro HCol1; [apply HCol1; exists S; Col|]. elim HPar1; clear HPar1; intro HCol2; [apply HCol2; exists S; spliter; Col|]. spliter; apply perp_not_col2 in HPerp3; elim HPerp3; intro HNC'; apply HNC'; Col. } { assert (O = PX) by (unfold Cong_3 in HCong1; spliter; treat_equalities; auto). treat_equalities; assert (HCol7 : Col S U2 P). { assert (H : Par P S S U2) by (apply l12_9_2D with S U1; Perp). elim H; clear H; intro H; [exfalso; apply H; exists S|spliter]; Col. } assert (HNC' : ~ Col S U1 U2) by (apply perp_not_col; Perp). assert (H : Rectangle P S QX' Q). { apply perp3__rect; try (intro; assert_diffs; apply HNC'; ColR); [apply perp_col0 with S U1|apply perp_sym; apply perp_col0 with S U1|]; Col; Perp. apply perp_sym; apply par_perp__perp with S U1; Perp. apply l12_9_2D with S U2; Perp. } apply Rectangle_Plg in H; apply plg_to_parallelogram in H; apply plg_cong_2 in H. unfold Cong_3 in HCong3; spliter; apply cong_transitivity with S QX'; Cong. } { assert (O = QX) by (unfold Cong_3 in HCong3; spliter; treat_equalities; auto). treat_equalities; assert (HCol7 : Col S U2 Q). { assert (H : Par Q S S U2) by (apply l12_9_2D with S U1; Perp). elim H; clear H; intro H; [exfalso; apply H; exists S|spliter]; Col. } assert (HNC' : ~ Col S U1 U2) by (apply perp_not_col; Perp). assert (H : Rectangle Q S PX' P). { apply perp3__rect; try (intro; assert_diffs; apply HNC'; ColR); [apply perp_col0 with S U1|apply perp_sym; apply perp_col0 with S U1|]; Col; Perp. apply perp_sym; apply par_perp__perp with S U1; Perp. apply l12_9_2D with S U2; Perp. } apply Rectangle_Plg in H; apply plg_to_parallelogram in H; apply plg_cong_2 in H. unfold Cong_3 in HCong1; spliter; apply cong_transitivity with S PX'; Cong. } { elim (eq_dec_points S PY'); intro HDiff3; treat_equalities. { assert (HNC' := HPerp3); apply perp_not_col2 in HNC'. elim HNC'; clear HNC'; intro HNC'; [exfalso; apply HNC'|intuition]. destruct HProjp2 as [H' H]; clear H'. elim H; clear H; intro H; [|spliter; subst; Col]. destruct H as [H HPerp5]; clear H. assert (HPar : Par P S S U1) by (apply l12_9_2D with S U2; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists S|spliter]; Col. } { assert (HNC' : ~ Col S U1 U2) by (apply perp_not_col; Perp). assert (HCol7 : Col S U1 PX') by (apply l4_13 with O E PX; Col). assert (HCol8 : Col S U2 PY') by (apply l4_13 with O E PY; Col). assert (HCol9 : Col S U1 QX') by (apply l4_13 with O E QX; Col). assert (HDiff4 : P <> PY'). { intro; treat_equalities; apply HDiff1. assert_diffs; apply l6_21 with S U1 U2 S; Col. assert (HPar : Par P PX' S U2) by (apply l12_9_2D with S U1; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists P|]; spliter; Col. } assert (HDiff5 : Q <> PY'). { intro; treat_equalities; apply HDiff2. assert_diffs; apply l6_21 with S U1 U2 S; Col. assert (HPar : Par Q QX' S U2) by (apply l12_9_2D with S U1; Perp). elim HPar; clear HPar; intro HPar; [exfalso; apply HPar; exists Q|]; spliter; Col. } assert (HRect1 : Rectangle PX' S PY' P). { apply perp3__rect; try (intro; assert_diffs; apply HNC'; ColR). { apply perp_col0 with S U2; Col. apply perp_col0 with S U1; Col; Perp. } { apply perp_col0 with P Q; try (apply perp_col0 with S U2); Col; Perp. apply col_permutation_1; apply projp2_col with S U2; auto. } { apply par_perp__perp with S U1; Perp. apply l12_9_2D with S U2; Perp. apply perp_sym; apply perp_col0 with P Q; Col. apply col_permutation_1; apply projp2_col with S U2; auto. } } assert (HRect2 : Rectangle QX' S PY' Q). { apply perp3__rect; try (intro; assert_diffs; apply HNC'; ColR). { apply perp_col0 with S U2; Col. apply perp_col0 with S U1; Col; Perp. } { apply perp_col0 with P Q; try (apply perp_col0 with S U2); Col; Perp. apply col_permutation_1; apply projp2_col with S U2; auto. } { apply par_perp__perp with S U1; Perp. apply l12_9_2D with S U2; Perp. apply perp_sym; apply perp_col0 with P Q; Col. apply col_permutation_1; apply projp2_col with S U2; auto. } } assert (HRect3 : Rectangle P PX' QX' Q) by (apply rect_2_rect with S PY'; try apply rect_permut; auto). apply Rectangle_Parallelogram in HRect3; apply plg_cong_2 in HRect3. assert_diffs; apply cong_3_2_cong_4 with O E PX QX S U1 PX' QX' in HCong1; Col. unfold Cong_4 in HCong1; spliter; apply cong_transitivity with PX' QX'; Cong. } } } { exfalso; elim (perp_not_col2 S U1 P PX'); Perp; intro H; apply H; Col; clear H. assert (HPar : Par P Q S U1) by (apply l12_9_2D with S U2; Perp). elim HPar; clear HPar; intro HPar; spliter; Col. exfalso; apply HPar; exists Q; Col. } { exfalso; elim (perp_not_col2 S U1 Q QX'); Perp; intro H; apply H; Col; clear H. assert (HPar : Par P Q S U1) by (apply l12_9_2D with S U2; Perp). elim HPar; clear HPar; intro HPar; spliter; Col. exfalso; apply HPar; exists P; Col. } { assert (Cong_4 O E PX QX S U1 P Q) by (assert_diffs; apply cong_3_2_cong_4; Col). unfold Cong_4 in *; spliter; Cong. } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths