proposition: Lemma existence_representant_vecteur : forall A B C : PO, ex (fun D : PO => vec A D = vec B C :>PP).
proof: Proof. unfold vec in |- *; intros. exists (barycentre (cons (-1) B) (cons 2 (barycentre (cons 1 A) (cons 1 C)))). replace 2 with (1 + 1) by ring. pattern 1 at 1 in |- *. RReplace 1 (-1 + 2). rewrite <-!add_PP_barycentre; try lra. RingPP. Qed.