proposition: Lemma puissance_cercle_tangente_rec : forall A B C O M : PO, triangle A B C -> circonscrit O A B C -> alignes A B M -> Rsqr (distance M C) = scalaire (vec M A) (vec M B) -> tangente_cercle O A C M.
proof: Proof. intros. deroule_circonscrit A B C O. deroule_triangle A B C. hcercle H0. symetrique O A A'. rewrite (scalaire_diametre (A:=A) (A':=A') (B:=B) (O:=O) (M:=M)) in H2; auto. elim (Pythagore C M O); intros. apply H15. rewrite (distance_sym C M). rewrite H2; rewrite H12. rewrite (distance_sym O C); ring. apply circonscrit_diametre with (1 := H0); auto. Qed.