proposition: Lemma trig_period_lemma (f : R -> R) (q : R) : q > 0 -> (forall x k, f (x + q * INR k) = f x) -> (forall x z, f (x + q * IZR z) = f x).
proof: Proof. intros Hq Hperiod x z. destruct z. - f_equal. lra. - rewrite <- (Hperiod x (Pos.to_nat p)). f_equal. rewrite INR_IZR_INZ. rewrite positive_nat_Z. reflexivity. - rewrite <- (Hperiod (x + q * IZR (Z.neg p)) (Pos.to_nat p)). f_equal. rewrite <- Rplus_0_r. rewrite Rplus_assoc. apply Rplus_eq_compat_l. rewrite <- Rmult_plus_distr_l. apply Rmult_eq_0_compat_l. rewrite INR_IZR_INZ. rewrite positive_nat_Z. rewrite <- plus_IZR. apply f_equal. lia. Qed.
imports: Coq(Reals.Ratan Lia Lra Logic.IndefiniteDescription Program.Subset) ZornsLemma(Quotients) Topology(ProductTopology AdjunctionSpace SubspaceTopology RTopology RFuncContinuity Homeomorphisms)