proposition: Lemma homothetie_conserve_contact_cercle_droite : forall (k : R) (I A A' B B' M M' O O' : PO), k <> 0 :>R -> A' = homothetie k I A :>PO -> B' = homothetie k I B :>PO -> M' = homothetie k I M :>PO -> O' = homothetie k I O -> tangente_cercle O A B M -> tangente_cercle O' A' B' M'.
proof: Proof. icercle. rewrite (distance_homothetie (k:=k) (I:=I) (A:=O) (A':=O') (B:=A) (B':=A')); auto. rewrite (distance_homothetie (k:=k) (I:=I) (A:=O) (A':=O') (B:=B) (B':=B')); auto. rewrite H5; auto. apply (homothetie_conserve_orthogonalite (k:=k) (I:=I) (A:=B) (A':=B') (B:=M) (B':=M') (M:=O) (M':=O')); auto. Qed.