proposition: Theorem caracterisation_cercle_diametre : forall A B M : PO, cercle_diametre A B M <-> scalaire (vec M A) (vec M B) = 0.
proof: Proof. red in |- *; try split; intros. hcercle H. elim H0; [ intros O H1; elim H1; [ intros H2 H3; try clear H1 H0; try exact H3 ] ]. discrimine A B. assert (A = M). apply cercle_diametre_degenere with B; auto. rewrite <- H1; rewrite H0. VReplace (vec B B) (mult_PP 0 (vec B B)). Simplscal. elim (classic (alignes A B M)); intros. elim alignes_diametre with (A := A) (B := M) (A' := B); intros; auto. rewrite H4. VReplace (vec A A) (mult_PP 0 (vec B B)). Simplscal. rewrite H4. VReplace (vec B B) (mult_PP 0 (vec B B)). Simplscal. assert (triangle A B M); (unfold triangle in |- *; auto). assert (orthogonal (vec M A) (vec M B)). apply (triangle_diametre (A:=M) (B:=A) (C:=B) (O:=O)); auto with geo. icercle. rewrite <- H6; auto. apply def_orthogonal; auto with geo. apply ligne_niveau_MAMB_O; auto. Qed.