proposition: Lemma homothetie_cercle_diametre : forall (k : R) (I A A' B B' M M' : PO), k <> 0 :>R -> A' = homothetie k I A :>PO -> B' = homothetie k I B :>PO -> M' = homothetie k I M :>PO -> cercle_diametre A B M -> cercle_diametre A' B' M'.
proof: Proof. icercle. elim H3; [ intros O H4; elim H4; [ intros H5 H6; elim H5; [ intros H7 H8; try clear H5 H4 H3; try exact H8 ] ] ]. elim existence_homothetique with (k := k) (I := I) (A := O); [ intros O' H3; try clear existence_homothetique; try exact H3 ]. exists O'; (split; auto). generalize (homothetie_bipoint (k:=k) (I:=I) (A:=O) (B:=A) (A':=O') (B':=A')); intros. generalize (homothetie_bipoint (k:=k) (I:=I) (A:=O) (B:=M) (A':=O') (B':=M')); intros. generalize (homothetie_bipoint (k:=k) (I:=I) (A:=O) (B:=B) (A':=O') (B':=B')); intros. split; apply carre_scalaire_egalite_distance. rewrite H4; auto. rewrite H9; auto. Simplscal. repeat rewrite carre_scalaire_distance; auto. rewrite H7; ring. rewrite H4; auto. rewrite H5; auto. Simplscal. repeat rewrite carre_scalaire_distance; auto. rewrite H8; ring. rewrite H3. rewrite (homothetie_milieu (k:=k) (I:=I) (A:=A) (A':=A') (B:=B) (B':=B') (M:=O) (N:=milieu A' B')); auto. Qed.