proposition: Lemma orthogonal_segment_milieu : forall A B C D I : PO, A <> B -> I = milieu A B -> orthogonal (vec A B) (vec C D) -> orthogonal (vec I A) (vec C D) /\ orthogonal (vec I B) (vec C D).
proof: Proof. intros. cut (orthogonal (vec A I) (vec C D)); intros. split; [ try assumption | idtac ]. VReplace (vec I A) (mult_PP (-1) (vec A I)). Simplortho. rewrite <- (milieu_vecteur (A:=A) (B:=B) (M:=I)); auto. rewrite (milieu_vecteur2 (A:=A) (B:=B) (M:=I)); auto. Simplortho. Qed.