proposition: Theorem rayon_Sinus: forall A B C O, triangle A 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. deroule_triangle A B C. soit_milieu B C A'. elim (classic (A' = O)); intros. apply diametre_Sinus; auto. rewrite <- H8; auto. apply rayon_Sinus_general with A'; auto. Qed.