proposition: Lemma t4Let3: t4 <= t3.
proof: Proof. Proof with auto with typeclass_instances. apply round_le... apply Rplus_le_compat_l. assert (0 <= round_flt (a - b)). rewrite ab_exact_. now apply Rle_0_minus. apply Rle_trans with (2:=H). rewrite <- Ropp_0. now apply Ropp_le_contravar. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)