proposition: Lemma centre_gravite_coplanaire : forall A B C : PO, ~ alignes A B C -> coplanaires A B C (centre_gravite A B C).
proof: Proof. unfold centre_gravite, milieu, coplanaires in |- *; intros. right; try assumption. exists (/ 3); exists (/ 3). cut (3 <> 0); intros; auto with real. apply mult_PP_regulier with 3; auto with real. FVReplace (mult_PP 3 (add_PP (cons (/ 3) A) (add_PP (cons (/ 3) B) (cons (1 + - (/ 3 + / 3)) C)))) (add_PP (cons 1 A) (add_PP (cons 1 B) (cons 1 C))) 3. VReplace (mult_PP 3 (cons 1 (barycentre (cons 1 A) (cons 2 (barycentre (cons 1 B) (cons 1 C)))))) (cons 3 (barycentre (cons 1 A) (cons 2 (barycentre (cons 1 B) (cons 1 C))))). replace 3 with (1 + 2) by ring. rewrite <- add_PP_barycentre; auto with real. replace 2 with (1 + 1) by ring. rewrite <- add_PP_barycentre; auto with real. Qed.