proposition: Lemma add_PP_milieu : forall A B : PO, add_PP (cons 1 A) (cons 1 B) = cons 2 (milieu A B) :>PP.
proof: Proof. unfold milieu in |- *; intros. replace 2 with (1 + 1) by ring. repeat rewrite <- add_PP_barycentre; auto. lra. Qed.