proposition: Lemma cercle_equation : forall (A M : PO) (r a b x y : R), a = abscisse A -> b = ordonnee A -> x = abscisse M -> y = ordonnee M -> cercle A r M -> Rsqr (x + - a) + Rsqr (y + - b) = Rsqr r.
proof: Proof. icercle. assert (scalaire (vec A M) (vec A M) = Rsqr r). rewrite carre_scalaire_distance; rewrite H3; auto. rewrite <- H4. assert (vec A M = add_PP (mult_PP (x + - a) (vec O I)) (mult_PP (y + - b) (vec O J))). apply composantes_vecAB; auto with geo. 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. Qed.