proposition: Lemma reflexion_conserve_contact_cercle_cercle : forall I J A A' B B' K K' O O' : PO, I <> J -> O <> A -> K <> B -> A' = reflexion I J A -> B' = reflexion I J B -> K' = reflexion I J K -> O' = reflexion I J O -> cercles_tangents O A K B -> cercles_tangents O' A' K' B'.
proof: Proof. intros. elim cercles_tangents_tangente_commune with (O := O) (A := A) (O' := K) (A' := B); [ intros T H7; elim H7; [ intros M H8; elim H8; [ intros H9 H10; elim H10; [ intros H11 H12; try clear H10 H8 H7; try exact H11 ] ] ] | auto | auto | auto ]. elim existence_reflexion_AB with (A := I) (B := J) (M := T); [ intros T' H7; try clear existence_reflexion_AB; try exact H7 | auto ]. elim existence_reflexion_AB with (A := I) (B := J) (M := M); [ intros M' H8; try clear existence_reflexion_AB; try exact H7 | auto ]. assert (distance O' A' = distance O A). rewrite <- (reflexion_isometrie (A:=I) (B:=J) (M:=O) (M':=O') (N:=A) (N':=A')) ; auto. assert (O' <> A'). apply (isometrie_distinct (A:=O) (B:=A) (A':=O') (B':=A')); auto. assert (distance K' B' = distance K B). rewrite <- (reflexion_isometrie (A:=I) (B:=J) (M:=K) (M':=K') (N:=B) (N':=B')) ; auto. assert (K' <> B'). apply (isometrie_distinct (A:=K) (B:=B) (A':=K') (B':=B')); auto. assert (distance T' M' = distance T M). rewrite <- (reflexion_isometrie (A:=I) (B:=J) (M:=T) (M':=T') (N:=M) (N':=M')) ; auto. assert (T' <> M'). apply (isometrie_distinct (A:=T) (B:=M) (A':=T') (B':=M')); auto. apply tangente_commune_cercles_tangents with (B := T') (M := M'); auto. apply reflexion_conserve_contact_cercle_droite with (2 := H2) (6 := H11); auto with geo. apply reflexion_conserve_contact_cercle_droite with (2 := H3) (6 := H12); auto with geo. Qed.