proposition: Lemma mediatrice_milieu_angles : forall A B M N : PO, A <> B -> M <> N -> M = milieu A B -> mediatrice A B N -> cons_AV (vec N A) (vec N M) = cons_AV (vec N M) (vec N B) :>AV.
proof: Proof. intros. elim mediatrice_distinct_extremite with (A := A) (B := B) (M := N); (auto; intros). cut (M <> A); intros. cut (M <> B); intros. elim cas_egalite_triangle_indirect with (A := M) (B := N) (C := A) (A' := M) (B' := N) (C' := B); (auto with geo; intros). elim H8; intros H9 H10; try clear H8; try exact H9. symmetry in |- *. generalize (milieu_angles_orthogonaux (A:=A) (B:=B) (M:=M) (N:=N)); intros. mesure M A M N. rewrite <- (mes_oppx (A:=M) (B:=A) (C:=M) (D:=N) (x:=x)); auto. rewrite <- (mes_oppx (A:=M) (B:=N) (C:=M) (D:=B) (x:=x)); auto. rewrite H8; rewrite H7; auto. apply mediatrice_orthogonale_segment_milieu; auto. lapply (milieu_distinct2 (A:=A) (B:=B)); auto; intros. rewrite H1; auto. lapply (milieu_distinct (A:=A) (B:=B)); auto; intros. rewrite H1; auto. Qed.