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