proposition: Lemma triangle_rectangle_cercle_diametre : forall A B C : PO, A <> B -> A <> C -> orthogonal (vec A B) (vec A C) -> cercle_diametre B C A.
proof: Proof. icercle. assert (triangle A B C). unfold triangle in |- *. apply orthogonal_non_alignes; auto. elim triangle_rectangle_demi_cercle with (A := A) (B := B) (C := C); [ intros O' H3; elim H3; [ intros H4 H5; try clear H3; try exact H5 ] | auto | auto ]. exists O'. hcercle H4. split; [ idtac | auto ]. rewrite <- H6; auto. assert (vec O' C = mult_PP (-1) (vec O' B)). deroule_circonscrit A B C O'. apply (alignes_distance_negatif_colineaire (k:=1) (A:=O') (B:=B) (C:=C)); auto. rewrite <- H6; rewrite <- H7; ring. apply egalite_vecteur_milieu. rewrite H3; Ringvec. Qed.