proposition: Lemma characterization_of_congruence_F : forall A B C D, Cong A B C D <-> let (Ac, _) := coordinates_of_point_F A in let (Ax, Ay) := Ac in let (Bc, _) := coordinates_of_point_F B in let (Bx, By) := Bc in let (Cc, _) := coordinates_of_point_F C in let (Cx, Cy) := Cc in let (Dc, _) := coordinates_of_point_F D in let (Dx, Dy) := Dc in (Ax - Bx) * (Ax - Bx) + (Ay - By) * (Ay - By) - ((Cx - Dx) * (Cx - Dx) + (Cy - Dy) * (Cy - Dy)) =F= 0.
proof: Proof. intros. elim (coordinates_of_point_F A); intros Ac HAc. elim (coordinates_of_point_F B); intros Bc HBc. elim (coordinates_of_point_F C); intros Cc HCc. elim (coordinates_of_point_F D); intros Dc HDc. destruct Ac as [[Ax HAx] [Ay HAy]]. destruct Bc as [[Bx HBx] [By HBy]]. destruct Cc as [[Cx HCx] [Cy HCy]]. destruct Dc as [[Dx HDx] [Dy HDy]]. rewrite subF__eq0; unfold AddF, MulF, SubF, EqF; simpl. destruct (diff_f Ax Bx HAx HBx) as [AxMBx HAxMBx]; simpl. destruct (prod_f AxMBx AxMBx (diff_col Ax Bx AxMBx HAxMBx) (diff_col Ax Bx AxMBx HAxMBx)) as [ABx HABx]; simpl. destruct (diff_f Ay By HAy HBy) as [AyMBy HAyMBy]; simpl. destruct (prod_f AyMBy AyMBy (diff_col Ay By AyMBy HAyMBy) (diff_col Ay By AyMBy HAyMBy)) as [ABy HABy]; simpl. destruct (sum_f ABx ABy (prod_col AxMBx AxMBx ABx HABx) (prod_col AyMBy AyMBy ABy HABy)) as [AB2 HAB2]; simpl. destruct (diff_f Cx Dx HCx HDx) as [CxMDx HCxMDx]; simpl. destruct (prod_f CxMDx CxMDx (diff_col Cx Dx CxMDx HCxMDx) (diff_col Cx Dx CxMDx HCxMDx)) as [CDx HCDx]. destruct (diff_f Cy Dy HCy HDy) as [CyMDy HCyMDy]; simpl. destruct (prod_f CyMDy CyMDy (diff_col Cy Dy CyMDy HCyMDy) (diff_col Cy Dy CyMDy HCyMDy)) as [CDy HCDy]; simpl. destruct (sum_f CDx CDy (prod_col CxMDx CxMDx CDx HCDx) (prod_col CyMDy CyMDy CDy HCDy)) as [CD2 HCD2]; simpl. apply (characterization_of_congruence O E E' SS U1 U2 A Ax Ay B Bx By C Cx Cy D Dx Dy AxMBx ABx AyMBy ABy AB2 CxMDx CDx CyMDy CDy CD2); auto. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems