proposition: Lemma milieu_angles : forall A B M N : PO, A <> B -> M <> N -> M = milieu A B -> cons_AV (vec M A) (vec M N) = plus (cons_AV (vec M B) (vec M N)) (image_angle pi) :>AV.
proof: Proof. intros. VReplace (vec M A) (mult_PP (-1) (vec A M)). rewrite <- (milieu_vecteur H1); auto. apply angle_produit_negatif_l; auto. cut (B <> M); intros; auto. rewrite H1; apply milieu_distinct; auto. rewrite H1; apply milieu_distinct2; auto. lra. Qed.