proposition: Lemma triangle_rectangle_demi_cercle : forall A B C : PO, triangle A B C -> orthogonal (vec A B) (vec A C) -> ex (fun O : PO => circonscrit O A B C /\ cons_AV (vec O B) (vec O C) = image_angle pi).
proof: Proof. intros; deroule_triangle A B C. soit_circonscrit A B C D. exists D. split; [ try assumption | idtac ]. rewrite <- (angle_inscrit (O:=D) (A:=A) (B:=B) (C:=C)); auto. apply orthogonal_angles; auto. Qed.