proposition: Lemma equation_tangente_cercle : 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 -> (c + - a) * (x + - c) + (d + - b) * (y + - d) = 0 -> tangente_cercle A C C M.
proof: Proof. icercle. assert (orthogonal (vec A C) (vec C M)). apply def_orthogonal2. 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. auto with geo. Qed.