proposition: Lemma axiom_A2a : forall A B r, A<>B -> exists P, AM_Col A B P /\ ratio A P A B =F= r.
proof: Proof. intros A B r. rewrite characterization_of_neq_F. unfold ratio,scalar_product. simpl. destruct ( let Ac:= proj1_sig (coordinates_of_point_F A) in let Ax := fst Ac in let Ay := snd Ac in let Bc:= proj1_sig (coordinates_of_point_F B) in let Bx := fst Bc in let By := snd Bc in point_of_coordinates O E SS U1 U2 (proj1_sig (Ax + r*(Bx-Ax))) (proj1_sig (Ay + r*(By-Ay))) orthonormal_grid (proj2_sig (Ax + r*(Bx-Ax))) (proj2_sig (Ay + r*(By-Ay)))) as [P HP]. exists P. revert HP. revert H. unfold AM_Col, twice_signed_area, cross_product. elim (coordinates_of_point_F A). simpl. elim (coordinates_of_point_F B). simpl. intros. simpl in *. destruct x0. destruct x. simpl in *. decompose_coordinates'. simpl in *. destruct (Cd_Cd_EqF P _ _ _ _ HP HP0) as [HA HB]. split. rewrite <- HA;rewrite <- HB;ring. rewrite <- HA;rewrite <- HB. 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