proposition: Theorem tangente_cercle_contact_unique : forall A B O M C : PO, B <> M -> tangente_cercle O A B M -> alignes B M C -> cercle_rayon O A C -> B = C.
proof: Proof. intros. hcercle H0. assert (B = projete_orthogonal B M O). apply def_projete_orthogonal; auto with geo. apply (unicite_contact_cercle_droite_tangente (A:=B) (B:=M) (O:=O) (D:=A) (H:=B) (C:=C)); auto. Qed.