proposition: Lemma mediatrice_projete_orthogonal : forall A B M H : PO, A <> B :>PO -> H = projete_orthogonal A B M :>PO -> mediatrice A B M -> distance H A = distance H B :>R.
proof: Proof. unfold mediatrice in |- *; intros. generalize (Pythagore_projete_orthogonal (A:=A) (B:=B) (C:=M) (H:=H)); intros. elim H3; [ try clear H3; intros | auto | auto ]. apply distance_carre. replace (Rsqr (distance H A)) with (Rsqr (distance A M) + - Rsqr (distance H M)). replace (Rsqr (distance H M)) with (Rsqr (distance B M) + - Rsqr (distance H B)). rewrite (distance_sym A M); auto. rewrite (distance_sym B M); auto. rewrite H2; ring. rewrite H4; ring. rewrite H3; ring. Qed.