proposition: Lemma ligne_niveau_MAMB_k : forall (A B I M : PO) (k : R), k + Rsqr (distance I A) >= 0 -> I = milieu A B -> scalaire (vec M A) (vec M B) = k -> cercle I (sqrt (k + Rsqr (distance I A))) M.
proof: Proof. intros A B I M k H H0; try assumption. rewrite (scalaire_difference_carre (A:=A) (B:=B) (I:=I) M); auto. icercle. assert (Rsqr (distance I M) = k + Rsqr (distance I A)). rewrite <- distance_sym; rewrite <- H1; ring. apply Rsqr_inj; auto with geo real. rewrite Rsqr_sqrt; auto with real. Qed.