proposition: Fact lt_0_Kdelta : 0 < Kdelta.
proof: Proof. exact: ubound_gt0. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp(bigenough cauchyreals) extra_mathcomp extra_cauchyreals tactics shift bigopz arithmetics seq_defs c_props s_props z3seq_props a_props b_props b_over_a_props