proposition: Lemma orthogonal_milieu : forall A B C D I : PO, A <> B -> I = milieu A B -> orthogonal (vec I A) (vec C D) \/ orthogonal (vec I B) (vec C D) -> orthogonal (vec A B) (vec C D).
proof: Proof. intros. elim H1; intros. replace (vec A B) with (mult_PP (-2) (vec I A)). Simplortho. replace (vec A B) with (add_PP (vec A I) (vec I B)). rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=I)); auto. Ringvec. Ringvec. replace (vec A B) with (mult_PP 2 (vec I B)). Simplortho. replace (vec A B) with (add_PP (vec A I) (vec I B)). rewrite (milieu_vecteur (A:=A) (B:=B) (M:=I)); auto. Ringvec. Ringvec. Qed.