proposition: Lemma diametre_Sinus: forall (A B C O : PO), triangle A B C -> O = milieu B C -> circonscrit O A B C -> distance B C = 2 * (distance O C * Rabs (Sin (cons_AV (vec A B) (vec A C)))).
proof: Proof. intros. assert (orthogonal (vec A B) (vec A C)). apply triangle_diametre with O; auto. deroule_triangle A B C. elim droit_direct_ou_indirect with ( A := A ) ( B := B ) ( C := C ); (intros; auto). rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=pisurdeux)); auto. rewrite sin_pisurdeux. rewrite Rabs_right; auto. rewrite (distance_double_milieu H0); ring. lra. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=- pisurdeux)); auto. rewrite sin_impaire. rewrite sin_pisurdeux. rewrite Rabs_left; auto. rewrite (distance_double_milieu H0); ring. lra. Qed.