proposition: Theorem sinA_sur_a_aire : forall (a b c sin_A sin_B sin_C S : R) (A B C : PO), triangle A B C -> a = distance B C -> b = distance A C -> c = distance A B -> S = aire_triangle A B C -> 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) /\ sin_A / a = 2 * S / (a * (b * c)).
proof: Proof. unfold aire_triangle in |- *; intros a b c d e f g A B C H H0 H1 H2 H3 H4 H5 H6. split; [ try assumption | idtac ]. apply sinA_sur_a with (1 := H); auto. deroule_triangle A B C. rewrite H0; rewrite H1; rewrite H2; rewrite H4; rewrite H3. rewrite def_aire; auto. rewrite Rabs_mult. rewrite Rabs_mult. rewrite (Rabs_right (distance A B)); auto with geo. rewrite (Rabs_right (distance A C)); auto with geo. rewrite <- H4; rewrite <- H2; rewrite <- H1; rewrite <- H0. field. rewrite H0; rewrite H1; rewrite H2. repeat split; auto with geo. Qed.