proposition: Lemma scalaire_diametre : forall A A' B O M : PO, A <> B -> O = milieu A A' -> cercle_diametre A A' B -> alignes A B M -> scalaire (vec M A) (vec M B) = Rsqr (distance M O) + - Rsqr (distance O A).
proof: Proof. intros A A' B O M H0 H1 H2 H3; try assumption. generalize H2; unfold cercle_diametre in |- *; intros. elim H4; [ intros O' H5; elim H5; [ intros H6 H7; try clear H5 H4; try exact H7 ] ]. assert (O' = O). rewrite H1; auto. rewrite H in H6; clear H O' H7. discrimine A A'. assert (A = B). apply cercle_diametre_degenere with A'; auto. rewrite <- H4. rewrite (scalaire_difference_carre (A:=A') (B:=A) (I:=O) M); auto with geo. elim (classic (alignes A A' B)); intros. assert (B = A'). elim alignes_diametre with (A := A) (B := B) (A' := A'); [ intros H12; try clear alignes_diametre | intros H12; try clear alignes_diametre; try exact H12 | auto | auto ]. absurd (A = B); auto. rewrite H5. rewrite (scalaire_difference_carre (A:=A) (B:=A') (I:=O) M); auto. assert (triangle A A' B); auto with geo. discrimine M A. unfold Rsqr in |- *; repeat rewrite <- carre_scalaire_distance. VReplace (vec A O) (mult_PP (-1) (vec O A)). VReplace (vec A A) (mult_PP 0 (vec O A)). Simplscal. rewrite <- (scalaire_avec_projete (A:=M) (B:=A) (C:=A') (H:=B)); auto. apply scalaire_difference_carre; auto. apply alignes_ordre_cycle2; auto. assert (orthogonal (vec B A) (vec B A')). apply triangle_diametre with O; auto with geo. apply circonscrit_permute; auto. halignes H3 k. replace (vec M A) with (mult_PP k (vec B A)). Simplortho. VReplace (vec M A) (mult_PP (-1) (vec A M)). rewrite H9; Ringvec. Qed.