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