proposition: Lemma alignes_mediatrice_milieu : forall A B M : PO, A <> B -> alignes A B M -> mediatrice A B M -> M = milieu A B :>PO.
proof: Proof. unfold mediatrice in |- *; intros. halignes H0 k. cut (k = / 2); intros. rewrite H3 in H2. apply vecteur_milieu; auto. cut (vec M B = mult_PP (1 + - k) (vec A B)); intros. cut (scalaire (vec A M) (vec A M) = scalaire (vec M B) (vec M B)); intros. rewrite H2 in H4. rewrite H3 in H4. cut (k * k = (1 + - k) * (1 + - k)); intros; auto with real. apply resolution2 with (x := scalaire (vec A B) (vec A B)) (y := scalaire (vec A B) (vec A B)); auto with geo. replace (scalaire (vec A B) (vec A B) * (k * k)) with (scalaire (mult_PP k (vec A B)) (mult_PP k (vec A B))). rewrite H4. Simplscal. ring_simplify. Simplscal. replace (scalaire (vec A M) (vec A M)) with (scalaire (vec M A) (vec M A)). repeat rewrite carre_scalaire_distance; rewrite H1; auto. replace (vec M A) with (mult_PP (-1) (vec A M)). Simplscal. Ringvec. replace (vec M B) with (add_PP (vec A B) (mult_PP (-1) (vec A M))). rewrite H2. Ringvec. Ringvec. Qed.