proposition: Lemma Pospow_lin_le_2pow: forall (n : positive), (2 * n <= 2 ^ n)%positive.
proof: Proof. intros n. induction n using Pos.peano_ind. - cbn. lia. - rewrite Pos.mul_succ_r, Pos.pow_succ_r. lia. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra