proposition: Fact NdeltaP (n : nat) : (Ndelta <= n)%N -> ((a n)%:CR * z3 - (b n)%:CR <= (Kdelta * (1 / a n))%:CR)%CR.
proof: Proof. by rewrite /Ndelta; case: delta_asympt => /= ?; exact. 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