proposition: Lemma square_distance_formula : forall O E E' S U1 U2 P Q PX PY QX QY PQ PQ2 PXMQX PYMQY PXMQX2 PYMQY2 F, Cd O E S U1 U2 P PX PY -> Cd O E S U1 U2 Q QX QY -> Is_length O E E' P Q PQ -> Prod O E E' PQ PQ PQ2 -> Diff O E E' PX QX PXMQX -> Prod O E E' PXMQX PXMQX PXMQX2 -> Diff O E E' PY QY PYMQY -> Prod O E E' PYMQY PYMQY PYMQY2 -> Sum O E E' PXMQX2 PYMQY2 F -> PQ2 = F.
proof: Proof. intros O E E' S U1 U2 P Q PX PY QX QY PQ PQ2 PXMQX PYMQY PXMQX2 PYMQY2 F. intros HCd1 HCd2 HPQ HPQ2 HPXMQX HPXMQX2 HPYMQY HPYMQY2 HF. assert (HNC : ~ Col O E E') by (apply diff_ar2 in HPXMQX; unfold Ar2 in *; spliter; Col). assert (HCol1 : Col O E PX) by (apply Cd_Col in HCd1; spliter; Col). assert (HCol2 : Col O E QX) by (apply Cd_Col in HCd2; spliter; Col). assert (HCol3 : Col O E PY) by (apply Cd_Col in HCd1; spliter; Col). assert (HCol4 : Col O E QY) by (apply Cd_Col in HCd2; spliter; Col). destruct (is_length_exists O E E' PX QX) as [PXQX HPXQX]; Col. assert (HCol5 : Col O E PXQX). { unfold Is_length, Length in HPXQX; induction HPXQX; spliter; treat_equalities; Col. } destruct (prod_exists O E E' HNC PXQX PXQX) as [PXQX2 HPXQX2]; Col. assert (PXQX2 = PXMQX2) by (apply l16_9_2 with O E E' PX QX PXQX PXMQX; Col). destruct (is_length_exists O E E' PY QY) as [PYQY HPYQY]; Col. assert (HCol6 : Col O E PYQY). { unfold Is_length, Length in HPYQY; induction HPYQY; spliter; treat_equalities; Col. } destruct (prod_exists O E E' HNC PYQY PYQY) as [PYQY2 HPYQY2]; Col. assert (PYQY2 = PYMQY2) by (apply l16_9_2 with O E E' PY QY PYQY PYMQY; Col). treat_equalities; apply sum_uniqueness with O E E' PXQX2 PYQY2; auto; clear HF; clear F. clear HPXMQX2; clear HPXMQX; clear PXMQX; clear HPYMQY2; clear HPYMQY; clear PYMQY. assert (HCs : Cs O E S U1 U2) by (unfold Cd in HCd1; spliter; auto). destruct (point_of_coordinates O E S U1 U2 PX QY) as [R HCd3]; Col. elim HPQ; clear HPQ; intro HPQ; [|spliter; treat_equalities; exfalso; Col]. elim HPXQX; clear HPXQX; intro HPXQX; [|spliter; treat_equalities; exfalso; Col]. elim HPYQY; clear HPYQY; intro HPYQY; [|spliter; treat_equalities; exfalso; Col]. elim (eq_dec_points P R); intro HPR; [assert (HPR' := HPR); rewrite eq_points_coordinates in HPR; [|apply HCd1|apply HCd3]|]; elim (eq_dec_points Q R); intro HQR; [assert (HQR' := HQR); rewrite eq_points_coordinates in HQR; [|apply HCd2|apply HCd3]| |assert (HQR' := HQR); rewrite eq_points_coordinates in HQR; [|apply HCd2|apply HCd3]|]; apply sum_comm; Col; apply pythagoras with P Q R PYQY PXQX PQ; auto; try intro; try (destruct HPR as [HPX HPY]); try (destruct HQR as [HQX HQY]); treat_equalities; Col; Perp; clear HPYQY2; clear HPXQX2; clear HPQ2; clear HPQ; try clear HPX; try clear HPY; try clear HQX; try clear HQY. { assert (O = PYQY); treat_equalities. { assert_diffs; apply length_uniqueness with O E E' PY PY; try apply length_id_2; auto. } assert_diffs; apply length_id_2; auto. } { assert (O = PXQX); treat_equalities. { assert_diffs; apply length_uniqueness with O E E' QX QX; try apply length_id_2; auto. } assert_diffs; apply length_id_2; auto. } { assert (O = PYQY); treat_equalities. { assert_diffs; apply length_uniqueness with O E E' PY PY; try apply length_id_2; auto. } assert_diffs; apply length_id_2; auto. } { apply square_distance_formula_aux with S U1 U2 PX PY QX; auto. } { apply square_distance_formula_aux with S U2 U1 QY QX PY; auto; try apply coord_exchange_axes; auto; try apply grid_exchange_axes; auto. apply length_sym; auto. } { assert (O = PXQX); treat_equalities. { assert_diffs; apply length_uniqueness with O E E' QX QX; try apply length_id_2; auto. } assert_diffs; apply length_id_2; auto. } { destruct HCd3 as [H [H' [HRX HRY]]]; clear H; clear H'; destruct HRX as [RX' [HProjp5 HCong5]]; destruct HRY as [RY' [HProjp6 HCong6]]; destruct HCd1 as [H [H' [HPX HPY]]]; clear H; clear H'; destruct HPX as [PX' [HProjp1 HCong1]]; destruct HPY as [PY' [HProjp2 HCong2]]; assert (RX' = PX') by (assert_diffs; apply col_cong_3_cong_3_eq with O E PX S U1; Col); subst; treat_equalities; destruct HCd2 as [H [H' [HQX HQY]]]; clear H; clear H'; destruct HQX as [QX' [HProjp3 HCong3]]; destruct HQY as [QY' [HProjp4 HCong4]]; assert (RY' = QY') by (assert_diffs; apply col_cong_3_cong_3_eq with O E QY S U2; Col); subst; assert (HPerp1 : Perp P R S U1) by (apply projp_projp_perp with PX'; auto); assert (HPerp2 : Perp Q R S U2) by (apply projp_projp_perp with QY'; auto); assert (HPerp3 : Perp U1 S S U2) by (unfold Cs in HCs; spliter; assert_diffs; apply per_perp; Perp). apply perp_per_2; apply perp_sym; apply par_perp__perp with S U1; Perp. apply l12_9_2D with S U2; Perp. } { apply square_distance_formula_aux with S U2 U1 QY PX PY; auto; try apply coord_exchange_axes; auto; try apply grid_exchange_axes; auto. apply length_sym; auto. } { apply length_sym. apply square_distance_formula_aux with S U1 U2 QX QY PX; auto. apply length_sym; auto. } Qed.
imports: GeoCoq.Tarski_dev.Ch15_lengths