proposition: Lemma Key_1b : forall k : nat, 1 <= k -> p3m k[*]eps [<=] Halfeps.
proof: Proof. intros. unfold Halfeps in |- *. apply mult_resp_leEq_rht. apply p3m_smaller. auto. apply less_leEq; apply eps_pos. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)