proposition: Lemma distance_similitude : forall (k a : R) (I A B A' B' : PO), k > 0 -> A' = similitude I k a A -> B' = similitude I k a B -> distance A' B' = k * distance A B.
proof: Proof. intros. elim similitude_decomposition with (I := I) (M := A) (M' := A') (k := k) (a := a); [ intros A1 H7; elim H7; intros H8 H9; try clear H7 | auto | auto ]. elim similitude_decomposition with (I := I) (M := B) (M' := B') (k := k) (a := a); [ intros B1 H7; elim H7; intros H10 H11; try clear H7; try exact H11 | auto | auto ]. cut (distance A1 B1 = distance A B); intros. rewrite <- H2. rewrite (distance_homothetie (k:=k) (I:=I) (A:=A1) (A':=A') (B:=B1) (B':=B')); auto. rewrite Rabs_right; auto. red in |- *; auto. apply rotation_isometrie with (1 := H8) (2 := H10). Qed.