proposition: Lemma distance_homothetie : forall (k : R) (I A A' B B' : PO), A' = homothetie k I A :>PO -> B' = homothetie k I B :>PO -> distance A' B' = Rabs k * distance A B.
proof: Proof. unfold distance in |- *; intros. rewrite <- sqrt_Rsqr_abs. rewrite <- sqrt_mult; intros. apply Rsqr_inj; auto with real geo. generalize (homothetie_bipoint (k:=k) (I:=I) (A:=A) (B:=B) (A':=A') (B':=B')); intros. replace (Rsqr k * scalaire (vec A B) (vec A B)) with (scalaire (mult_PP k (vec A B)) (mult_PP k (vec A B))). rewrite H1; auto. unfold Rsqr; Simplscal. auto with real. generalize scalaire_positif; intros; auto with real. Qed.