proposition: Lemma barycentre_zero : forall (a : R) (A B : PO), a <> 0 -> barycentre (cons a A) (cons 0 B) = A.
proof: Proof. intros a A B H; try assumption. apply conversion_PP with (a := a + 0) (b := a); try ring; auto. repeat rewrite <- add_PP_barycentre; auto. RingPP. unfold not in |- *; intros H1; apply H; auto; rewrite <- H1; ring; auto. replace (a + 0) with a; try ring; auto. Qed.