proposition: Lemma chasles_ratios : forall A B C P Q, P <> Q -> ratio A B P Q + ratio B C P Q =F= ratio A C P Q.
proof: Proof. intros A B C P Q. rewrite characterization_of_neq_F. unfold ratio, scalar_product. decompose_coordinates;simpl. intro. field. intro. apply H. rewrite <- H0. ring. Qed.
imports: Description Ring Field Nsatz Rtauto GeoCoq.Tarski_dev.Ch16_coordinates GeoCoq.Tarski_dev.Ch15_pyth_rel GeoCoq.Tarski_dev.Annexes.midpoint_theorems