proposition: Lemma colineaire_barycentre : forall (k : R) (A B C : PO), vec A C = mult_PP k (vec A B) -> C = barycentre (cons (1 + - k) A) (cons k B).
proof: Proof. unfold vec in |- *; intros. elim cons_inj with (a := 1) (b := 1 + - k + k) (A := C) (B := barycentre (cons (1 + - k) A) (cons k B)); intros; auto with *. repeat rewrite <- add_PP_barycentre; auto. RingPP2 H. RingPP. replace (1 + - k + k) with 1; try ring; auto with *. Qed.