proposition: Lemma triangle_diametre : forall A B C O : PO, triangle A B C -> O = milieu B C -> circonscrit O A B C -> orthogonal (vec A B) (vec A C).
proof: Proof. intros. apply triangle_demi_cercle_rectangle with O; auto. deroule_circonscrit A B C O. replace (cons_AV (vec O B) (vec O C)) with (plus (cons_AV (vec O B) (vec O A)) (cons_AV (vec O A) (vec O C))). deroule_triangle A B C. rewrite (milieu_angles (A:=B) (B:=C) (M:=O) (N:=A)); auto. rewrite <- (def_opp (A:=O) (B:=A) (C:=O) (D:=C)); auto. mesure O A O C. RReplace (- x + pi + x) pi; auto. rewrite Chasles; auto. Qed.