proposition: Lemma triangle_demi_cercle_rectangle : forall A B C O : PO, triangle A B C -> circonscrit O A B C -> cons_AV (vec O B) (vec O C) = image_angle pi -> orthogonal (vec A B) (vec A C).
proof: Proof. intros; deroule_triangle A B C. deroule_circonscrit A B C O. apply angles_orthogonal; auto. rewrite (angle_inscrit (O:=O) (A:=A) (B:=B) (C:=C)); auto. Qed.