proposition: Lemma rotation_conserve_contact_cercle_droite : forall (I A A' B B' M M' O O' : PO) (a : R), A' = rotation I a A -> B' = rotation I a B -> M' = rotation I a M -> O' = rotation I a O -> tangente_cercle O A B M -> tangente_cercle O' A' B' M'.
proof: Proof. icercle. rewrite (rotation_isometrie (I:=I) (A:=O) (B:=A) (A':=O') (B':=A') (a:=a)); auto. rewrite (rotation_isometrie (I:=I) (A:=O) (B:=B) (A':=O') (B':=B') (a:=a)); auto. apply (rotation_conserve_orthogonalite (I:=I) (A:=B) (B:=M) (M:=O) (A':=B') (B':=M') (M':=O') (a:=a)); auto. Qed.