proposition: Lemma homogene_barycentre : forall (a b k : R) (A B : PO), a + b <> 0 -> k <> 0 -> barycentre (cons (k * a) A) (cons (k * b) B) = barycentre (cons a A) (cons b B).
proof: Proof. intros a b k A B H H0; try assumption. apply conversion_PP with (a := k * a + k * b) (b := k * (a + b)); try ring; auto. repeat rewrite <- add_PP_barycentre; auto. rewrite distrib_mult_cons. rewrite <- def_mult_PP. repeat rewrite <- add_PP_barycentre; auto. replace (k * a + k * b) with (k * (a + b)); try ring. auto with *. replace (k * a + k * b) with (k * (a + b)); try ring. auto with *. Qed.