fact: Definition ratio 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 let VAB := (Bx-Ax, By-Ay) in let VCD := (Dx-Cx, Dy-Cy) in scalar_product VAB VCD / scalar_product VCD VCD.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems