proposition: Theorem intersection_cercle_droite : forall A B O D H : PO, A <> B -> H = projete_orthogonal A B O -> distance O H <= distance O D -> exists C : PO, alignes A B C /\ cercle_rayon O D C.
proof: Proof. icercle. assert (Rsqr (distance O D) + - Rsqr (distance O H) >= 0). unfold Rsqr in |- *. RReplace (distance O D * distance O D + - (distance O H * distance O H)) ((distance O D + - distance O H) * (distance O D + distance O H)). assert (distance O D >= 0); auto with geo. assert (distance O H >= 0); auto with geo. assert (distance O D + distance O H >= 0). lra. assert (distance O D + - distance O H >= 0). lra. RReplace 0 (0 * (distance O D + distance O H)). apply Rmult_ge_compat_r; auto. elim def_projete_orthogonal2 with (A := A) (B := B) (C := O) (H := H); [ intros; auto | auto | auto ]. discrimine H A. assert (H <> B). contrapose H0. rewrite <- H7; auto. elim existence_intersection_droite_cercle_centre with (r := sqrt (Rsqr (distance O D) + - Rsqr (distance O H))) (A := H) (B := B); [ intros C H8; elim H8; [ intros H9 H10; try clear H8; try exact H10 ] | auto | auto ]. exists C; split; auto. assert (Rsqr (distance O D) = Rsqr (distance O C)). elim (Pythagore H O C); intros. rewrite H8; auto. replace (Rsqr (distance H C)) with (distance H C * distance H C); auto with real. rewrite H10. rewrite sqrt_sqrt; auto with real. rewrite (distance_sym H O); ring. halignes H9 k. apply ortho_sym. rewrite H12; pattern H at 1 in |- *; rewrite H6; auto with geo. auto with real. apply Rsqr_inj; auto with geo real. auto with real. elim existence_intersection_droite_cercle_centre with (r := sqrt (Rsqr (distance O D) + - Rsqr (distance O H))) (A := H) (B := A); [ intros C H8; elim H8; [ intros H9 H10; try clear H8; try exact H10 ] | auto | auto ]. exists C; split; auto. halignes H9 k. halignes H4 k'. apply colineaire_alignes with (k' + - (k * k')). VReplace (vec A C) (add_PP (vec A H) (vec H C)). rewrite H7. VReplace (vec H A) (mult_PP (-1) (vec A H)). rewrite H8; Ringvec. assert (Rsqr (distance O D) = Rsqr (distance O C)). elim (Pythagore H O C); intros. rewrite H7; auto. replace (Rsqr (distance H C)) with (distance H C * distance H C); auto with real. rewrite H10. rewrite sqrt_sqrt; auto with real. rewrite (distance_sym H O); ring. halignes H9 k. halignes H4 k'. apply ortho_sym. rewrite H11. VReplace (vec H A) (mult_PP (-1) (vec A H)). rewrite H12. VReplace (mult_PP k (mult_PP (-1) (mult_PP k' (vec A B)))) (mult_PP (- (k * k')) (vec A B)). auto with geo. apply Rsqr_inj; auto with geo real. auto with real. Qed.