proposition: Lemma trivial_sin_Sin : forall (A B C D : PO) (x : R), distance A B = 1 -> distance A C = 1 -> image_angle x = cons_AV (vec A B) (vec A C) -> repere_orthonormal_direct A B D -> sin x = Sin (cons_AV (vec A B) (vec A C)).
proof: Proof. intros. rewrite (def_sin (A:=A) (B:=B) (C:=C) (D:=D) (x:=x)); auto. rewrite (def_Sin (A:=A) (B:=B) (C:=C) (D:=D)); auto. Qed.