proposition: Lemma barycentre_mes_alg : forall (a b : R) (A B G : PO), a + b <> 0 :>R -> G = barycentre (cons a A) (cons b B) :>PO -> a * mes_alg G A + b * mes_alg G B = 0 :>R.
proof: Proof. intros. cut (a <> 0 \/ b <> 0); intros. elim H1; [ intros H2; try clear H1 | intros H2; try clear H1; try exact H2 ]. cut (mes_alg G A = / a * - b * mes_alg G B); intros. rewrite H1. RReplace (a * (/ a * - b * mes_alg G B)) (a * / a * (- b * mes_alg G B)). RReplace (a * / a) 1. ring. apply def_mes_alg. apply mult_PP_regulier with a; auto. replace (mult_PP a (mult_PP (/ a * - b) (vec G B))) with (add_PP (mult_PP (- b) (vec G B)) zero). rewrite <- (def_vecteur_bary (a:=a) (b:=b) (A:=A) (B:=B) (G:=G)); auto. Ringvec. Fieldvec a. cut (mes_alg G B = / b * - a * mes_alg G A); intros. rewrite H1. RReplace (b * (/ b * - a * mes_alg G A)) (b * / b * (- a * mes_alg G A)). RReplace (b * / b) 1. ring. apply def_mes_alg. apply mult_PP_regulier with b; auto. replace (mult_PP b (mult_PP (/ b * - a) (vec G A))) with (add_PP (mult_PP (- a) (vec G A)) zero). rewrite <- (def_vecteur_bary (a:=a) (b:=b) (A:=A) (B:=B) (G:=G)); auto. Ringvec. Fieldvec b. apply not_and_or. red in |- *; intros; apply H. elim H1; intros H2 H3; try clear H1; try exact H3. rewrite H2; rewrite H3; ring. Qed.