proposition: Lemma circle_cover_preimage t0 t1 : circle_cover t0 = circle_cover t1 -> exists z : Z, t0 - t1 = IZR z.
proof: Proof. unfold circle_cover. intros. inversion H; subst; clear H. destruct (euclidian_division t0 1) as [k0 [r0 [H00 H01]]]. { pose proof PI_neq0. lra. } destruct (euclidian_division t1 1) as [k1 [r1 [H10 H11]]]. { pose proof PI_neq0. lra. } subst. rewrite !Rmult_1_r in *. rewrite !Rmult_plus_distr_l in *. rewrite Rplus_comm in H1. rewrite cos_period_Z in H1. rewrite Rplus_comm in H1. rewrite cos_period_Z in H1. rewrite Rplus_comm in H2. rewrite sin_period_Z in H2. rewrite Rplus_comm in H2. rewrite sin_period_Z in H2. cut (r0 = r1). { intros. subst. exists (k0 - k1)%Z. rewrite <- Z_R_minus. lra. } rewrite Rabs_R1 in *. eapply circle_cover_inj; try lra. unfold circle_cover. congruence. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)