proposition: Lemma equation_cartesienne_cercle : forall (M : PO) (x y a b r : R), r >= 0 -> x = abscisse M -> y = ordonnee M -> Rsqr (x + - a) + Rsqr (y + - b) = Rsqr r -> exists A : _, cercle A r M.
proof: Proof. icercle. assert (vec O M = add_PP (mult_PP x (vec O I)) (mult_PP y (vec O J))); auto with geo. elim existence_representant_comb_lin_vecteur with (A := O) (B := I) (C := O) (D := J) (a := a) (b := b); intros A H4. exists A. assert (vec A M = add_PP (mult_PP (x + - a) (vec O I)) (mult_PP (y + - b) (vec O J))); auto with geo. apply composantes_vecAB; eauto with geo. assert (scalaire (vec A M) (vec A M) = Rsqr r). rewrite (scalaire_composantes_ABCD (O:=O) (I:=I) (J:=J) (A:=A) (B:=M) (C:=A) (D:=M) (x:=x + - a) (y:=y + - b) (x':=x + - a) (y':=y + - b)) ; auto with geo. rewrite carre_scalaire_distance in H6. apply Rsqr_inj; auto with geo real. Qed.