proposition: Lemma milieu_parallelogrammme_rec: forall (A B C D I : PO), I = milieu A C -> I = milieu B D -> vec A B = vec D C.
proof: Proof. unfold vec; intros. assert (add_PP (cons 1 B) (cons 1 D) = add_PP (cons 1 A) (cons 1 C)). repeat rewrite add_PP_milieu. rewrite <- H. rewrite <- H0; auto. RingPP1 H1. RingPP. Qed.