proposition: Lemma existence_representant_comb_lin_vecteur : forall (A B C D : PO) (a b : R), ex (fun E : PO => vec A E = add_PP (mult_PP a (vec A B)) (mult_PP b (vec C D)) :>PP).
proof: Proof. intros. elim existence_representant_mult_vecteur with (A := A) (B := A) (C := B) (k := a); intros B' H; try clear existence_representant_mult_vecteur; rewrite <- H. elim existence_representant_mult_vecteur with (A := C) (B := C) (C := D) (k := b); intros C' H0; try clear existence_representant_mult_vecteur; rewrite <- H0. elim existence_representant_som_vecteur with (A := A) (B := B') (C := C) (D := C'); intros E H1; try clear existence_representant_som_vecteur; rewrite <- H1. exists E; auto. Qed.