proposition: Lemma characterization_of_collinearity_F : forall A B C, Col A B C <-> 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 (Ax - Bx) * (By - Cy) - (Ay - By) * (Bx - Cx) =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. destruct Ac as [[Ax HAx] [Ay HAy]]. destruct Bc as [[Bx HBx] [By HBy]]. destruct Cc as [[Cx HCx] [Cy HCy]]. rewrite subF__eq0; unfold AddF, MulF, SubF, EqF; simpl. destruct (diff_f Ax Bx HAx HBx) as [AxMBx HAxMBx]; simpl. destruct (diff_f By Cy HBy HCy) as [ByMCy HByMCy]; simpl. destruct (prod_f AxMBx ByMCy (diff_col Ax Bx AxMBx HAxMBx) (diff_col By Cy ByMCy HByMCy)) as [P1 HP1]; simpl. destruct (diff_f Ay By HAy HBy) as [AyMBy HAyMBy]; simpl. destruct (diff_f Bx Cx HBx HCx) as [BxMCx HBxMCx]; simpl. destruct (prod_f AyMBy BxMCx (diff_col Ay By AyMBy HAyMBy) (diff_col Bx Cx BxMCx HBxMCx)) as [P2 HP2]; simpl. apply (characterization_of_collinearity O E E' SS U1 U2 A Ax Ay B Bx By C Cx Cy AxMBx AyMBy BxMCx ByMCy P1 P2); 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