proposition: Lemma concours_3_mediane : forall A B C : PO, concours_3 A (milieu B C) (milieu A B) C (milieu A C) B.
proof: Proof. intros A B C; try assumption. generalize (add_PP_milieu_asso A B C); intros. generalize (add_PP_milieu_permute A B C); intros. unfold concours_3 in |- *. exists (barycentre (cons 1 A) (cons 2 (milieu B C))). split; [ try assumption | idtac ]. apply barycentre_alignes; try discrR; auto with *. split; [ try assumption | idtac ]. apply add_PP_alignes with (a := 2) (b := 1); try discrR; auto with *. rewrite <- H; auto. rewrite add_PP_barycentre; try discrR; auto with *. apply cons_comp; (try ring; auto). apply add_PP_alignes with (a := 2) (b := 1); try discrR; auto with *. rewrite <- H0; auto. rewrite add_PP_barycentre; try discrR; auto with *. apply cons_comp; try ring; auto. Qed.