proposition: Lemma Qdlog_bounded_nonneg (b : nat) (n : Z) (x : Q) : 0 ≤ Qdlog_bounded b n x.
proof: Proof. revert x. induction b; unfold Qdlog_bounded; [reflexivity |]. intros. case (decide_rel); intros; [reflexivity |]. apply semirings.nonneg_plus_compat ; [easy | apply IHb]. Qed.
imports: Coq.ZArith.ZArith Coq.QArith.QArith Coq.QArith.Qround CoRN.stdlib_omissions.Q MathClasses.interfaces.abstract_algebra MathClasses.interfaces.additional_operations MathClasses.interfaces.orders MathClasses.theory.int_pow MathClasses.orders.rationals MathClasses.implementations.stdlib_rationals MathClasses.implementations.positive_semiring_elements