proposition: Lemma Qdlog2_le1 (n : Z) (x : Q) : 2 ≤ n → x ≤ 1 → Qdlog n x = 0.
proof: Proof. intros En Ex. unfold Qdlog. generalize (Z.abs_nat (Qdlog2 x)). intros b. induction b; simpl; [reflexivity |]. case (decide_rel); intros E; [reflexivity |]. destruct E. apply orders.le_lt_trans with 1; try assumption. apply orders.lt_le_trans with 2. now apply semirings.lt_1_2. now apply (order_preserving (cast Z Q)) in En. 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