proposition: Lemma barycentre_concours : forall (a b c d : R) (A B C D I : PO), A <> B -> C <> D :>PO -> a + b <> 0 :>R -> barycentre (cons a A) (cons b B) = I :>PO -> c + d <> 0 :>R -> barycentre (cons c C) (cons d D) = I :>PO -> concours (droite A B) (droite C D).
proof: Proof. intros a b c d A B C D I H H0 H1 H2 H3 H4; try assumption. apply def_concours with I; auto. rewrite <- H2. apply barycentre_alignes; auto. rewrite <- H4. apply barycentre_alignes; auto. Qed.