proposition: Theorem sinA_sur_a : forall (a b c sin_A sin_B sin_C : R) (A B C : PO), triangle A B C -> a = distance B C -> b = distance A C -> c = distance A B -> sin_A = Rabs (Sin (cons_AV (vec A B) (vec A C))) -> sin_B = Rabs (Sin (cons_AV (vec B C) (vec B A))) -> sin_C = Rabs (Sin (cons_AV (vec C A) (vec C B))) -> sin_A / a = sin_B / b /\ sin_A / a = sin_C / c.
proof: Proof. intros. rewrite H0; rewrite H1; rewrite H2; rewrite H5; rewrite H4; rewrite H3. deroule_triangle A B C. split; [ try assumption | idtac ]. replace (Rabs (Sin (cons_AV (vec A B) (vec A C)))) with (/ distance A B * / distance A C * (distance B C * (distance B A * Rabs (Sin (cons_AV (vec B C) (vec B A)))))). replace (distance A B) with (distance B A); auto with geo. field; repeat split; auto with geo. rewrite <- produit_longueur_absolu_Sin; auto. field; split; auto with geo. replace (Rabs (Sin (cons_AV (vec A B) (vec A C)))) with (/ distance A B * / distance A C * (distance C A * (distance C B * Rabs (Sin (cons_AV (vec C A) (vec C B)))))). replace (distance A C) with (distance C A); auto with geo. replace (distance B C) with (distance C B); auto with geo. field; repeat split; auto with geo. rewrite <- produit_longueur_absolu_Sin2; auto. field; split; auto with geo. Qed.