proposition: Lemma Qpower_2powneg_le_inv: forall (n : positive), (2 * 2 ^ Z.neg n <= 1 # n)%Q.
proof: Proof. intros n. induction n using Pos.peano_ind. - cbn. lra. - rewrite <- Pos2Z.opp_pos, Pos2Z.inj_succ, Z.opp_succ, Pos2Z.opp_pos, <- Z.sub_1_r. rewrite Qpower_minus_pos. ring_simplify. apply (Qmult_le_l _ _ (1#2)) in IHn. 2: lra. ring_simplify in IHn. apply (Qle_trans _ _ _ IHn). unfold Qle, Qmult, Qnum, Qden. ring_simplify; rewrite Pos2Z.inj_succ, <- Z.add_1_l. clear IHn; induction n using Pos.peano_ind. + reflexivity. + rewrite Pos2Z.inj_succ, <- Z.add_1_l. rewrite <- POrderedType.Positive_as_OT.add_1_l. rewrite POrderedType.Positive_as_OT.mul_add_distr_l. rewrite Pos2Z.inj_add. apply Z.add_le_mono. * lia. * exact IHn. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra