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