proposition: Lemma t4pos: 0 <= t4.
proof: Proof. Proof with auto with typeclass_instances. apply FLX_pos_is_pos. apply Rle_0_minus. apply round_le_generic... apply Rplus_le_reg_l with b; ring_simplify. exact isaTriangle1. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)