proposition: Lemma concours_barycentre : forall A B C D : PO, A <> B -> C <> D -> concours (droite A B) (droite C D) -> exists I : PO, ex (fun a : R => ex (fun b : R => I = barycentre (cons (1 + - a) A) (cons a B) :>PO /\ I = barycentre (cons (1 + - b) C) (cons b D) :>PO)).
proof: Proof. intros A B C D H10 H11 H; try assumption. elim def_concours2 with (3 := H); auto. intros I H0; elim H0; intros H1 H2; clear H0 H; try exact H2. elim alignes_barycentre with (A := A) (B := B) (C := I); [ intros a H; try clear alignes_barycentre; try exact H | auto | auto ]. elim alignes_barycentre with (A := C) (B := D) (C := I); [ intros b H'; try clear alignes_barycentre | auto | auto ]. exists I; exists (1 + - a); exists (1 + - b). replace (1 + - (1 + - a)) with a; try ring. replace (1 + - (1 + - b)) with b; try ring. split; [ try assumption | try assumption ]. Qed.