proposition: Lemma equation_k_cercle : forall (A A' K M : PO) (k a b a' b' x y : R), k + Rsqr (distance K A) >= 0 -> a = abscisse A -> b = ordonnee A -> a' = abscisse A' -> b' = ordonnee A' -> x = abscisse M -> y = ordonnee M -> K = milieu A A' -> (x + - a) * (x + - a') + (y + - b) * (y + - b') = k -> cercle K (sqrt (k + Rsqr (distance K A))) M.
proof: Proof. intros A A' K M k a b a' b' x y H H0 H1 H2 H3 H4 H5 H6; try assumption. 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. replace (scalaire (vec A M) (vec A' M)) with (scalaire (vec M A) (vec M A')). intros. apply ligne_niveau_MAMB_k with A'; auto. VReplace (vec M A) (mult_PP (-1) (vec A M)). VReplace (vec M A') (mult_PP (-1) (vec A' M)). Simplscal. apply composantes_vecAB; eauto with geo. apply composantes_vecAB; eauto with geo. Qed.