proposition: Lemma homothetie_vecteur : forall (k : R) (I A A' : PO), A' = homothetie k I A -> vec I A' = mult_PP k (vec I A).
proof: Proof. unfold homothetie, vec in |- *; intros. rewrite H. pattern 1 at 1 in |- *. replace 1 with (k + (1 + - k)); try ring. repeat rewrite <- add_PP_barycentre; try discrR. RingPP. replace (k + (1 + - k)) with 1; try ring. try discrR. Qed.