proposition: Lemma triangle_rectangle_direct_Sin : forall A B C : PO, A <> B -> A <> C -> B <> C -> image_angle pisurdeux = cons_AV (vec B C) (vec B A) -> distance C B = distance C A * Sin (cons_AV (vec A B) (vec A C)).
proof: Proof. intros. mes (cons_AV (vec A B) (vec A C)). rewrite <- H3. rewrite <- (egalite_sin_Sin (A:=A) (B:=B) (C:=C) (x:=x)); auto. apply triangle_rectangle_direct_sinus; auto. Qed.