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