proposition: Lemma existence_representant_mult_vecteur : forall (A B C : PO) (k : R), ex (fun D : PO => vec A D = mult_PP k (vec B C) :>PP).
proof: Proof. intros. elim (classic (k = -1)); intros. rewrite H. elim existence_representant_vecteur with (A := A) (B := C) (C := B); intros D H0; try clear existence_representant_vecteur; try exact H0. exists D. rewrite H0; Ringvec. unfold vec in |- *. exists (barycentre (cons (- k) B) (cons (1 + k) (barycentre (cons 1 A) (cons k C)))). pattern 1 at 1 in |- *. RReplace 1 (- k + (1 + k)). repeat rewrite <- add_PP_barycentre; try lra. RingPP. Qed.