proposition: Lemma p3m_smaller : forall i : nat, 0 < i -> p3m i [<=] Half.
proof: Proof. intros. apply leEq_transitive with (p3m 1). apply p3m_mon'. auto with arith. unfold p3m in |- *. astepl ([1] [/]ThreeNZ:IR). unfold Half in |- *. apply less_leEq. apply recip_resp_less. apply pos_two. apply two_less_three. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)