proposition: Theorem intersection2_cercle_droite : forall A B O H : PO, A <> B -> O <> A -> H = projete_orthogonal A B O -> distance O H < distance O A -> exists C : PO, A <> C /\ alignes A B C /\ cercle_rayon O A C.
proof: Proof. icercle. assert (Rsqr (distance O A) + - Rsqr (distance O H) > 0). unfold Rsqr in |- *. assert (distance O A <> 0); auto with geo. cut (distance O A >= 0); auto with geo. unfold Rge in |- *; intros. elim H5; [ intros H6; try clear H5 | intros H6; absurd (distance O A = 0); auto ]. RReplace (distance O A * distance O A + - (distance O H * distance O H)) ((distance O A + - distance O H) * (distance O A + distance O H)). assert (0 < distance O A + - distance O H). lra. assert (0 < distance O A + distance O H). apply Rplus_lt_le_0_compat; auto with real geo. assert (0 < (distance O A + - distance O H) * (distance O A + distance O H)). apply Rmult_lt_0_compat; auto with real. lra. elim def_projete_orthogonal2 with (A := A) (B := B) (C := O) (H := H); [ intros; auto | auto | auto ]. assert (H <> A). assert (distance O H <> distance O A); auto with real. contrapose H7. rewrite <- H8; auto. halignes H5 k. elim existence_symetrique with (A := H) (B := A); (intros C; intros). assert (H = milieu A C); auto with geo. assert (vec A C = mult_PP 2 (vec A H)); auto with geo. exists C; split; auto. generalize (distinct_produit_vecteur (A:=A) (B:=H) (C:=C) (a:=2)); intros H18; apply H18; auto with real geo. split; [ idtac | try assumption ]. apply colineaire_alignes with (2 * k). rewrite H11; rewrite H8; Ringvec. assert (Rsqr (distance O A) = Rsqr (distance O C)). elim (Pythagore H O C); intros. rewrite H12; auto. replace (Rsqr (distance H C)) with (Rsqr (distance H A)). elim (Pythagore H O A); intros. rewrite H14; auto. apply ortho_sym. replace (vec H A) with (mult_PP (- k) (vec A B)). auto with geo. VReplace (vec H A) (mult_PP (-1) (vec A H)). rewrite H8; Ringvec. rewrite (milieu_distance H10); auto. replace (vec H C) with (vec A H). apply ortho_sym. rewrite H8; auto with geo. auto with geo. auto with geo. Qed.