fact: Axiom def_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 = scalaire (vec A C) (vec A D).