fact: Axiom droit_direct_ou_indirect : forall A B C : PO, A <> B -> A <> C -> orthogonal (vec A B) (vec A C) -> image_angle pisurdeux = cons_AV (vec A B) (vec A C) \/ image_angle (- pisurdeux) = cons_AV (vec A B) (vec A C).