proposition: Lemma concours_mediane : forall A B C : PO, A <> milieu B C :>PO -> milieu A B <> C :>PO -> concours (droite A (milieu B C)) (droite (milieu A B) C).
proof: Proof. intros A B C H H0; try assumption. generalize (add_PP_milieu_asso A B C); intros. generalize (add_PP_concours (a:=1) (b:=2) (c:=2) (d:=1) (A:=A) (B:= milieu B C) (C:=milieu A B) (D:=C) (I:=barycentre (cons 1 A) (cons 2 (milieu B C)))); intros H8; apply H8; auto. try discrR; auto with *. rewrite add_PP_barycentre; try discrR; auto with *. try discrR; auto with *. rewrite <- H1; auto. rewrite add_PP_barycentre; try discrR; auto with *. apply cons_comp; try ring; auto. Qed.