proposition: Lemma rep_interval_auxiliary: forall b l u r1 r2, r2 <= u -> r1 <= u -> l <= r2 -> l <= r1 -> u - l <= b-> -b <= r1-r2 <= b.
proof: Proof. intros; split; fourier. Qed.
imports: Reals QArithSternBrocot(R_addenda) Fourier