proposition: Lemma prop_vecteur_bary_rec : forall (a b : R) (A B G M : PO), a + b <> 0 -> add_PP (mult_PP a (vec M A)) (mult_PP b (vec M B)) = mult_PP (a + b) (vec M G) -> G = barycentre (cons a A) (cons b B).
proof: Proof. unfold vec in |- *; intros. apply conversion_PP with (a := a + b) (b := a + b); auto. rewrite <- (add_PP_barycentre (a:=a) (b:=b) A B); auto. cut (add_PP (cons (- (a + b)) M) (cons (a + b) G) = add_PP (mult_PP a (add_PP (cons (-1) M) (cons 1 A))) (mult_PP b (add_PP (cons (-1) M) (cons 1 B)))); intros. RingPP2 H1. RingPP. rewrite H0. RingPP. Qed.