proposition: Lemma equation_generale_cercle : forall (M : PO) (x y a b c : R), c + (Rsqr a + Rsqr b) >= 0 -> x = abscisse M -> y = ordonnee M -> Rsqr x + (Rsqr y + (2 * (a * x) + 2 * (b * y))) = c -> exists A : _, cercle A (sqrt (c + (Rsqr a + Rsqr b))) M.
proof: Proof. intros M x y a b c H H0 H1; try assumption. RReplace (Rsqr x + (Rsqr y + (2 * (a * x) + 2 * (b * y)))) (Rsqr x + 2 * (a * x) + (Rsqr y + 2 * (b * y))). replace (Rsqr x + 2 * (a * x)) with (Rsqr (x + a) + - Rsqr a). replace (Rsqr y + 2 * (b * y)) with (Rsqr (y + b) + - Rsqr b). intros; assert (Rsqr (x + - - a) + Rsqr (y + - - b) = c + (Rsqr a + Rsqr b)). RReplace (x + - - a) (x + a). RReplace (y + - - b) (y + b). rewrite <- H2; ring. apply (equation_cartesienne_cercle (M:=M) (x:=x) (y:=y) (a:= - a) (b:=- b) (r:=sqrt (c + (Rsqr a + Rsqr b)))); auto with real. rewrite Rsqr_sqrt; auto with real. rewrite Rsqr_plus; ring. rewrite Rsqr_plus; ring. Qed.