proposition: Lemma def_vecteur_bary_rec : forall (a b : R) (A B G : PO), a + b <> 0 -> add_PP (mult_PP a (vec G A)) (mult_PP b (vec G B)) = zero -> 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. replace (cons (a + b) G) with (add_PP (cons (a + b) G) zero). rewrite <- H0. RingPP. RingPP. Qed.