proposition: Lemma add_PP_milieu_asso : forall A B C : PO, add_PP (cons 1 A) (cons 2 (milieu B C)) = add_PP (cons 2 (milieu A B)) (cons 1 C) :>PP.
proof: Proof. intros A B C; try assumption. repeat rewrite <- add_PP_milieu; try discrR; auto. RingPP. Qed.