proposition: Lemma translation_conserve_orthogonalite : forall I J A A' B B' M M' : PO, A' = translation I J A -> B' = translation I J B -> M' = translation I J M -> orthogonal (vec A B) (vec A M) -> orthogonal (vec A' B') (vec A' M').
proof: Proof. intros. rewrite <- (translation_bipoint (I:=I) (J:=J) (A:=A) (A':=A') (B:=M) (B':=M')) ; auto. rewrite <- (translation_bipoint (I:=I) (J:=J) (A:=A) (A':=A') (B:=B) (B':=B')) ; auto. Qed.