proposition: Lemma centre_gravite_ordre_cycle2 : forall A B C : PO, centre_gravite A B C = centre_gravite C A B :>PO.
proof: Proof. unfold centre_gravite in |- *; intros. generalize (add_PP_milieu_asso A B C); intros. apply conversion_PP with (a := 3) (b := 3); auto with *. replace 3 with (1 + 2) by ring. rewrite <- add_PP_barycentre; try discrR; auto with *. rewrite <- add_PP_barycentre; try discrR; auto with *. rewrite H. RingPP. Qed.