proposition: Lemma caract_milieu_parallelogramme: forall (A B C D : PO), (milieu A C = milieu B D <-> parallelogramme A B C D).
proof: Proof. intros. elim (existence_milieu A C); [intros I H; (try clear existence_milieu)]. rewrite <- H. unfold parallelogramme; split; intros. apply milieu_parallelogrammme_rec with I; auto. eapply milieu_parallelogrammme;eauto. Qed.