proposition: Lemma orthogonal_pisurdeux_or : forall A B C D : PO, A <> B -> C <> D -> orthogonal (vec A B) (vec C D) -> image_angle pisurdeux = cons_AV (vec A B) (vec C D) \/ image_angle (- pisurdeux) = cons_AV (vec A B) (vec C D).
proof: Proof. intros A B C D H H0; try assumption. elim existence_representant_vecteur with (A := A) (B := C) (C := D); [ intros E H2; rewrite <- H2; intros ]. apply droit_direct_ou_indirect; auto. apply distinct_egalite_vecteur with (2 := H2); auto. Qed.