proposition: Lemma angles_milieu : forall A B C I : PO, B <> C :>PO -> B <> A :>PO -> I = milieu B C :>PO -> cons_AV (vec B C) (vec B A) = cons_AV (vec B I) (vec B A) :>AV.
proof: Proof. intros. replace (vec B C) with (mult_PP 2 (vec B I)); auto with geo. apply angle_produit_positif_l; auto. rewrite H1; apply milieu_distinct; auto. lra. rewrite <- (milieu_vecteur_double (A:=B) (B:=C) (M:=I)); auto. Qed.