proposition: Lemma barycentre_alignes : forall (a b : R) (A B : PO), a + b <> 0 -> alignes A B (barycentre (cons a A) (cons b B)).
proof: Proof. intros a b A B H; try assumption. apply add_PP_alignes with (a := a) (b := b); auto with geo. Qed.