proposition: Theorem egalite_puissance_cocycliques : forall A B C D M : PO, triangle A B C -> M <> C -> alignes A B M -> alignes C D M -> scalaire (vec M A) (vec M B) = scalaire (vec M C) (vec M D) -> sont_cocycliques A B C D.
proof: Proof. unfold sont_cocycliques in |- *; intros A B C D M H10 H0 H1 H2 H3. elim existence_cercle_circonscrit with (A := A) (B := B) (C := C); [ intros O H4; try clear existence_cercle_circonscrit; try exact H4 | auto ]. exists O; split; auto. elim existence_projete_orthogonal with (A := M) (B := C) (C := O); [ intros H H6; try clear existence_projete_orthogonal; try exact H6 | auto ]. elim def_projete_orthogonal2 with (A := M) (B := C) (C := O) (H := H); [ intros; auto | auto | auto ]. assert (alignes M C D); auto with geo. halignes H8 k'. halignes H5 k. discrimine H C. assert (Rsqr (distance M C) = scalaire (vec M A) (vec M B)). apply puissance_cercle_tangente with O; auto. hcercle H4. rewrite <- H12. replace (vec H M) with (mult_PP (- k) (vec M C)). auto with geo. VReplace (vec H M) (mult_PP (-1) (vec M H)). rewrite H11; Ringvec. assert (k' = 1). apply Rmult_eq_reg_l with (scalaire (vec M C) (vec M C)); auto with geo. replace (scalaire (vec M C) (vec M C) * k') with (scalaire (vec M C) (vec M D)). rewrite carre_scalaire_distance. unfold Rsqr in H13. rewrite H13; rewrite H3; ring. rewrite H9; Simplscal. assert (D = C). apply egalite_vecteur_point with M. rewrite H9; rewrite H14; Ringvec. rewrite H15; auto. elim intersection2_cercle_droite with (A := C) (B := M) (O := O) (H := H); [ intros E H13; elim H13; [ intros H14 H15; elim H15; [ unfold cercle_rayon, isocele in |- *; intros H16 H17; try clear H15 H13; try exact H17 ] ] | auto | auto | auto | auto ]. assert (sont_cocycliques A B C E). exists O; split; auto. generalize H4; unfold circonscrit, isocele in |- *; intros; applatit_and. split; [ try assumption | idtac ]. rewrite <- H17; auto. assert (scalaire (vec M C) (vec M D) = scalaire (vec M C) (vec M E)). rewrite <- H3. apply puissance_cercle; auto. auto with geo. assert (alignes M C E); auto with geo. halignes H18 k1. assert (k' = k1). apply Rmult_eq_reg_l with (scalaire (vec M C) (vec M C)); auto with geo. replace (scalaire (vec M C) (vec M C) * k') with (scalaire (vec M C) (vec M D)). rewrite H15; rewrite H19; Simplscal. rewrite H9; Simplscal. assert (D = E). apply egalite_vecteur_point with M. rewrite H9; rewrite H20; rewrite H19; auto. rewrite H21. generalize H13; unfold sont_cocycliques in |- *; intros. elim H22; [ intros O1 H23; elim H23; [ intros H24 H25; try clear H23 H22; try exact H25 ] ]. assert (O1 = O). apply (unicite_circonscrit_triangle H10 H24 H4); auto. rewrite H22 in H25; auto. deroule_circonscrit A B C O. try exact H15. apply def_projete_orthogonal; auto with geo. apply projete_distance_Rlt with M; auto. Qed.