proposition: Lemma t1pos_: 0 <= t1.
proof: Proof. Proof with auto with typeclass_instances. apply FLT_pos_is_pos. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); apply Rle_trans with (1:=cLeb); exact bLea. apply FLT_pos_is_pos. apply Rplus_le_le_0_compat. apply Rle_trans with (1:=cPos); exact cLeb. exact cPos. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)