proposition: Lemma t2Let1: t2 <= t1.
proof: Proof. Proof with auto with typeclass_instances. apply round_le... apply Rplus_le_compat_l. apply round_le... apply Rplus_le_compat_l. apply Rle_trans with (2:=cPos). rewrite <- Ropp_0. now apply Ropp_le_contravar. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)