proposition: Lemma homothetie_cercle : forall (k : R) (I A A' O O' M M' : PO), k <> 0 :>R -> O' = homothetie k I O :>PO -> A' = homothetie k I A :>PO -> M' = homothetie k I M :>PO -> cercle O (distance O A) M -> cercle O' (distance O' A') M'.
proof: Proof. unfold cercle in |- *; intros. generalize (homothetie_bipoint (k:=k) (I:=I) (A:=O) (B:=M) (A':=O') (B':=M')); intros H5. generalize (homothetie_bipoint (k:=k) (I:=I) (A:=O) (B:=A) (A':=O') (B':=A')); intros. apply carre_scalaire_egalite_distance. rewrite H5; auto. rewrite H4; auto. Simplscal. repeat rewrite carre_scalaire_distance; auto. rewrite H3; ring. Qed.