proposition: Lemma centre_gravite_ordre_permute : forall A B C : PO, centre_gravite A B C = centre_gravite A C B :>PO.
proof: Proof. unfold centre_gravite in |- *; intros. rewrite (milieu_permute (A:=C) (B:=B) (I:=milieu C B)); auto. Qed.