proposition: Theorem loi_Sinus: forall A B C, triangle A B C -> and (distance B C / Rabs (Sin (cons_AV (vec A B) (vec A C))) = distance A B / Rabs (Sin (cons_AV (vec C A) (vec C B)))) (distance B C / Rabs (Sin (cons_AV (vec A B) (vec A C))) = distance C A / Rabs (Sin (cons_AV (vec B C) (vec B A)))).
proof: Proof. intros. deroule_triangle A B C. soit_rayon_circonscrit A B C D a. rewrite (rayon_Sinus (A:=A) (B:=B) (C:=C) (O:=D)); auto. rewrite <- H5; auto. generalize H4; unfold circonscrit, isocele; intros. elim H6; [intros H7 H8; (try clear H6); (try exact H8)]. split; [try assumption | idtac]. rewrite (rayon_Sinus (A:=C) (B:=A) (C:=B) (O:=D)); auto with geo. rewrite <- H7; rewrite H8; rewrite H5. field. split; auto with geo. apply circonscrit_permute; auto. rewrite (rayon_Sinus (A:=B) (B:=C) (C:=A) (O:=D)); auto with geo. rewrite H8; rewrite H5. field. split; auto with geo. unfold circonscrit, isocele. split; auto. rewrite <- H7; rewrite H8; auto. Qed.