proposition: Lemma homothetie_conserve_orthogonalite : forall (k : R) (I A A' B B' M M' : PO), k <> 0 :>R -> A' = homothetie k I A :>PO -> B' = homothetie k I B :>PO -> M' = homothetie k I M :>PO -> orthogonal (vec A B) (vec A M) -> orthogonal (vec A' B') (vec A' M').
proof: Proof. intros. generalize (homothetie_bipoint (k:=k) (I:=I) (A:=A) (B:=B) (A':=A') (B':=B')); intros. generalize (homothetie_bipoint (k:=k) (I:=I) (A:=A) (B:=M) (A':=A') (B':=M')); intros. assert (orthogonal (vec A B) (vec A' M')). apply ortho_sym; rewrite H5; auto with geo. rewrite H4; auto with geo. Qed.