proposition: Lemma co_side : forall A B C P, A <> C -> ~ twice_signed_area P A C =F= 0 -> twice_signed_area A B C =F= 0 -> ratio A B A C =F= twice_signed_area P A B / twice_signed_area P A C.
proof: Proof. intros A B C P. intro HAC. setoid_rewrite characterization_of_neq_F in HAC. unfold twice_signed_area, ratio. decompose_coordinates. unfold cross_product, scalar_product;simpl. intros. assert ( ((Bx - Ax) * (Cx - Ax) + (By - Ay) * (Cy - Ay)) * ((Ax - Px) * (Cy - Py) - (Ay - Py) * (Cx - Px)) =F= ((Ax - Px) * (By - Py) - (Ay - Py) * (Bx - Px)) * ((Cx - Ax) * (Cx - Ax) + (Cy - Ay) * (Cy - Ay))). put_negs_in_goal. express_disj_as_a_single_poly. assert (H2 : - Bx * Cy =F= - Bx * Ay - Ax * Cy + Ax * By + Ay * Cx - By * Cx) by nsatz. now ring [H2]. apply field_prop. intro. apply HAC. rewrite <- H2. ring. assumption. rewrite H1. 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