proposition: Lemma unicite_contact_cercle_droite_tangente : forall A B O D H C : PO, A <> B -> H = projete_orthogonal A B O -> cercle_rayon O D H -> alignes A B C -> cercle_rayon O D C -> H = C.
proof: Proof. icercle. elim def_projete_orthogonal2 with (A := A) (B := B) (C := O) (H := H); [ intros; auto | auto | auto ]. elim (Pythagore H O C); intros. assert (distance H C = 0); auto with geo. apply Rsqr_inj; auto with geo real. assert (Rsqr (distance O C) + - Rsqr (distance H O) = 0). rewrite (distance_sym H O). rewrite <- H4; rewrite <- H2; (unfold Rsqr in |- *; ring). replace (Rsqr 0) with 0; [ idtac | unfold Rsqr in |- *; ring ]. rewrite <- H9; rewrite H7; auto. unfold Rsqr in |- *; ring. halignes H3 x. halignes H5 y. apply ortho_sym. replace (vec H C) with (mult_PP (x + - y) (vec A B)); auto with geo. VReplace (vec H C) (add_PP (vec A C) (mult_PP (-1) (vec A H))). rewrite H11; rewrite H10; Ringvec. Qed.