proposition: Lemma similitude_conserve_contact_cercle_droite : forall (I A B M A' B' M' O O' : PO) (k a : R), k > 0 -> A' = similitude I k a A -> B' = similitude I k a B -> M' = similitude I k a M -> O' = similitude I k a O -> tangente_cercle O A B M -> tangente_cercle O' A' B' M'.
proof: Proof. icercle. rewrite (distance_similitude (k:=k) (a:=a) (I:=I) (A:=O) (B:=A) (A':=O') (B':=A')) ; auto. rewrite (distance_similitude (k:=k) (a:=a) (I:=I) (A:=O) (B:=B) (A':=O') (B':=B')) ; auto. rewrite H5; auto. apply (similitude_conserve_orthogonalite (I:=I) (A:=B) (B:=M) (M:=O) (A':=B') (B':=M') (M':=O') (k:=k) (a:=a)); auto. Qed.