proposition: Lemma cercle_diametre_equation : forall (A A' M : PO) (a b a' b' x y : R), a = abscisse A -> b = ordonnee A -> a' = abscisse A' -> b' = ordonnee A' -> x = abscisse M -> y = ordonnee M -> cercle_diametre A A' M -> (x + - a) * (x + - a') + (y + - b) * (y + - b') = 0.
proof: Proof. intros. elim (caracterisation_cercle_diametre A A' M); intros. rewrite <- H6; auto. 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. VReplace (vec A M) (mult_PP (-1) (vec M A)). VReplace (vec A' M) (mult_PP (-1) (vec M A')). Simplscal. apply composantes_vecAB; eauto with geo. apply composantes_vecAB; eauto with geo. Qed.