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