proposition: Lemma triangle_sin_not_0: forall A B C x, triangle A B C -> image_angle x = cons_AV (vec A B) (vec A C) -> (sin x <> 0).
proof: Proof. intros. deroule_triangle A B C. rewrite (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto. auto with geo. Qed.