fact: Axiom egalite_double_abs_Sin : forall A B C E F G, double_AV (cons_AV (vec A B) (vec A C)) = double_AV (cons_AV (vec E F) (vec E G)) -> Rabs (Sin (cons_AV (vec A B) (vec A C))) = Rabs (Sin (cons_AV (vec E F) (vec E G))).