proposition: Lemma Rbar_mult_p_l y (Hy : 0 < y) : Rbar_mult y p_infty = p_infty.
proof: Proof. rewrite /Rbar_mult /Rbar_mult'. case: (Rle_dec 0 y) => Hy1; last by lra. by case: (Rle_lt_or_eq_dec 0 y Hy1) => // ; lra. Qed.
imports: Coq(Reals ZArith Psatz Fourier_util) Flocq(Raux) Coquelicot(Coquelicot AutoDerive) mathcomp.ssreflect(ssreflect ssrfun ssrbool ssrnat bigop) Stdlib Coquelicot Xreal Interval