proposition: Lemma existence_intersection_droite_cercle_centre : forall (r : R) (A B : PO), A <> B -> r >= 0 -> exists C : PO, alignes A B C /\ distance A C = r.
proof: Proof. intros. assert (distance A B <> 0); auto with geo. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := / distance A B * r); intros C H2. exists C. split; [ try assumption | idtac ]. apply (colineaire_alignes H2); auto. assert (Rsqr (distance A C) = Rsqr r). unfold Rsqr in |- *; repeat rewrite <- carre_scalaire_distance. rewrite H2. Simplscal. rewrite carre_scalaire_distance. field. auto with real. auto with real. apply Rsqr_inj; auto with geo real. Qed.