proposition: Lemma t3Let2: t3 <= t2.
proof: Proof. Proof with auto with typeclass_instances. apply round_le... rewrite ab_exact_. apply Rle_trans with (a+(c-b));[right; ring|idtac]. apply Rplus_le_compat_l. apply Rle_trans with 0%R. now apply Rle_minus. apply FLT_pos_is_pos. now apply Rle_0_minus. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)