proposition: Lemma distance_double_milieu: forall (B C A' : PO), A' = milieu B C -> distance B C = 2 * distance A' C.
proof: Proof. intros. rewrite <- (milieu_distance H); auto. assert (vec B C = mult_PP 2 (vec B A')). apply milieu_vecteur_double; auto. rewrite (distance_sym A' B). RReplace 2 (Rabs 2). apply colinearite_distance; auto. rewrite Rabs_right; auto. lra. Qed.