proposition: Theorem puissance_cercle_tangente : forall A B C O M : PO, triangle A B C -> circonscrit O A B C -> alignes A B M -> tangente_cercle O A C M -> Rsqr (distance M C) = scalaire (vec M A) (vec M B).
proof: Proof. unfold tangente_cercle in |- *; intros; applatit_and. symetrique O A A'. deroule_triangle A B C. deroule_circonscrit A B C O. hcercle H0. clear H3. rewrite (scalaire_diametre (A:=A) (A':=A') (B:=B) (O:=O) (M:=M)); auto. elim (Pythagore C O M); intros. replace (Rsqr (distance O A)) with (Rsqr (distance O C)). rewrite (distance_sym M O). rewrite H3; auto with geo. rewrite (distance_sym M C); rewrite (distance_sym O C); ring. rewrite <- H15; auto. apply circonscrit_diametre with (1 := H0); auto. Qed.