proposition: Lemma axiom_A2b : forall A B P P' r, A<>B -> Col A B P -> ratio A P A B =F= r -> Col A B P' -> ratio A P' A B =F= r -> P = P'.
proof: Proof. intros A B P P' r. rewrite characterization_of_neq_F. rewrite characterization_of_equality_F. rewrite characterization_of_collinearity_F. rewrite characterization_of_collinearity_F. unfold ratio, scalar_product in *. simpl in *. decompose_coordinates. intros. split. apply field_prop_1 in H1; apply field_prop_1 in H3. put_negs_in_goal; express_disj_as_a_single_poly. nsatz. intro;apply H;rewrite <- H4;ring. intro;apply H;rewrite <- H4;ring. intro;apply H;rewrite <- H4;ring. apply field_prop_1 in H1; apply field_prop_1 in H3. put_negs_in_goal; express_disj_as_a_single_poly. nsatz. intro;apply H;rewrite <- H4;ring. intro;apply H;rewrite <- H4;ring. intro;apply H;rewrite <- H4;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