proposition: Lemma tangente_cercle_equation : forall (A C M : PO) (a b c d x y : R), a = abscisse A -> b = ordonnee A -> c = abscisse C -> d = ordonnee C -> x = abscisse M -> y = ordonnee M -> tangente_cercle A C C M -> (c + - a) * (x + - c) + (d + - b) * (y + - d) = 0.
proof: Proof. icercle. rewrite <- (scalaire_composantes_ABCD (O:=O) (I:=I) (J:=J) (A:=A) (B:=C) (C:=C) (D:=M) (x:=c + - a) (y:=d + - b) (x':=x + - c) (y':=y + - d)) ; auto with geo. apply composantes_vecAB; eauto with geo. apply composantes_vecAB; eauto with geo. Qed.