proposition: Lemma alignes_barycentre : forall A B C : PO, A <> B -> alignes A B C -> exists k : R, C = barycentre (cons k A) (cons (1 + - k) B).
proof: Proof. unfold alignes, alignes1 in |- *; intros. elim H0; [ intros H1; tauto | intros H1; elim H1; [ intros k H2; try clear H1 H0; try exact H2 ] ]. exists k; auto. apply conversion_PP with (a := 1) (b := k + (1 + - k)); try ring; auto with *. rewrite H2; auto. repeat rewrite <- add_PP_barycentre; auto. replace (k + (1 + - k)) with 1; try ring; auto with *. Qed.