proposition: Lemma rayon_Sinus_general: forall (A B C A' O : PO), triangle A B C -> O <> A' -> A' = 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. deroule_triangle A B C. deroule_circonscrit A B C O. assert (orthogonal (vec O A') (vec B C)). apply milieu_centrecirconscrit_orthogonal_segment with A; auto. rewrite (distance_double_milieu H1). replace (distance O C * Rabs (Sin (cons_AV (vec A B) (vec A C)))) with (distance C O * Rabs (Sin (cons_AV (vec O A') (vec O C)))). rewrite <- triangle_rectangle_absolu_Sin; auto. rewrite (distance_sym A' C); auto. rewrite H1. generalize (milieu_distinct2 H5); auto. apply ortho_sym. rewrite <- (milieu_vecteur H1); auto. rewrite (milieu_vecteur2 H1); auto. Simplortho. rewrite distance_sym. assert (double_AV (cons_AV (vec A B) (vec A C)) = double_AV (cons_AV (vec O A') (vec O C))). apply demi_angle_centre; auto. rewrite (egalite_double_abs_Sin H11); auto. Qed.