proposition: Lemma reflexion_conserve_contact_cercle_droite : forall I J A A' B B' M M' O O' : PO, I <> J -> A' = reflexion I J A -> B' = reflexion I J B -> M' = reflexion I J M -> O' = reflexion I J O -> tangente_cercle O A B M -> tangente_cercle O' A' B' M'.
proof: Proof. icercle. rewrite <- (reflexion_isometrie (A:=I) (B:=J) (M:=O) (M':=O') (N:=A) (N':=A')) ; auto. rewrite <- (reflexion_isometrie (A:=I) (B:=J) (M:=O) (M':=O') (N:=B) (N':=B')) ; auto. apply (reflexion_conserve_orthogonalite (I:=I) (J:=J) (A:=B) (A':=B') (B:=M) (B':=M') (M:=O) (M':=O')); auto. Qed.