proposition: Lemma circle_cover_inj t0 t1 : 0 <= t0 < 1 -> 0 <= t1 < 1 -> circle_cover t0 = circle_cover t1 -> t0 = t1.
proof: Proof. intros. pose proof PI_RGT_0. assert (forall x, 0 <= x < 1 -> 0 <= 2 * PI * x < 2 * PI). { intros. split. - apply Rmult_le_pos; lra. - rewrite <- Rmult_1_r. apply Rmult_lt_compat_l; lra. } apply H3 in H. apply H3 in H0. apply (Rmult_eq_reg_l (2*PI)); try lra. apply pair_equal_spec in H1. destruct H1, (Rle_or_lt (2 * PI * t0) PI), (Rle_or_lt (2 * PI * t1) PI). - apply cos_inj; lra. - apply sin_ge_0 in H5; try lra. apply sin_lt_0 in H6; lra. - apply sin_ge_0 in H6; try lra. apply sin_lt_0 in H5; lra. - apply Ropp_eq_compat in H1. rewrite <- neg_cos_PI, <- neg_cos_PI in H1. apply cos_inj in H1; lra. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)