proposition: Theorem puissance_cercle : forall A B C D M : PO, triangle A B C -> C <> D -> sont_cocycliques A B C D -> alignes A B M -> alignes C D M -> scalaire (vec M A) (vec M B) = scalaire (vec M C) (vec M D).
proof: Proof. intros A B C D M H H20 H0 H2 H3; try assumption. elim cocycliques_existence_diametre with (A := A) (B := B) (C := C) (D := D); [ intros A' H1; try clear cocycliques_existence_diametre; try exact H1 | auto ]. generalize H0; generalize H1; unfold sont_cocycliques, diametre_circonscrit in |- *; intros. elim H4; [ intros O1 H6; elim H6; [ intros H7 H8; try clear H6 H4; try exact H8 ] ]. elim H5; [ intros O H4; elim H4; [ intros H6 H9; try clear H4 H5; try exact H9 ] ]. assert (O1 = O). apply (unicite_circonscrit_triangle H H8 H6); auto. rewrite H4 in H7; clear H8 H4. deroule_triangle A B C. deroule_circonscrit A B C O. rewrite (scalaire_diametre (A:=A) (A':=A') (B:=B) (O:=O) (M:=M)); auto. hcercle H9; hcercle H6. replace (Rsqr (distance O A)) with (Rsqr (distance O C)). symetrique O C C'. rewrite (scalaire_diametre (A:=C) (A':=C') (B:=D) (O:=O) (M:=M)); auto. apply changement_diametre with (2 := H6); auto. rewrite <- H18; auto. apply circonscrit_diametre with (1 := H6); auto. Qed.