proposition: Lemma concours_3_barycentre : forall (a b c : R) (A B C : PO), a + (b + c) <> 0 :>R -> a + b <> 0 :>R -> b + c <> 0 :>R -> a + c <> 0 :>R -> concours_3 A (barycentre (cons b B) (cons c C)) (barycentre (cons a A) (cons b B)) C (barycentre (cons a A) (cons c C)) B.
proof: Proof. unfold concours_3 in |- *. intros a b c A B C H H0 H1 H2; try assumption. exists (barycentre (cons a A) (cons (b + c) (barycentre (cons b B) (cons c C)))). generalize (add_PP_assoc (cons a A) (cons b B) (cons c C)); intros. generalize (add_PP_assoc_permute (cons a A) (cons b B) (cons c C)); intros. split; [ try assumption | idtac ]. apply add_PP_alignes with (a := a) (b := b + c); auto with geo. split; [ try assumption | idtac ]. apply add_PP_alignes with (a := a + b) (b := c); auto with geo. unfold not in |- *; intros; apply H. rewrite <- H5; ring. rewrite <- add_PP_barycentre; auto with geo. rewrite <- H3; auto. repeat rewrite add_PP_barycentre; auto with geo. apply cons_comp; auto. ring. apply add_PP_alignes with (a := a + c) (b := b); auto with geo. unfold not in |- *; intros; apply H. rewrite <- H5; ring. rewrite <- add_PP_barycentre; auto. rewrite <- H4; auto. repeat rewrite add_PP_barycentre; auto. apply cons_comp; auto. ring. Qed.