proposition: Lemma colinearite_distance : forall (k : R) (A B C D : PO), vec C D = mult_PP k (vec A B) :>PP -> distance C D = Rabs k * distance A B.
proof: Proof. unfold distance in |- *; intros. rewrite H; Simplscal. replace (k * k) with (Rsqr k); auto with real. rewrite sqrt_mult; auto with real geo. rewrite sqrt_Rsqr_abs; ring. Qed.