proposition: Lemma p3m_S : forall i : nat, p3m (S i) [=] p3m i [/]ThreeNZ.
proof: Proof. intros. unfold p3m in |- *. astepl (([1] [/]ThreeNZ) [^]i[*] ([1] [/]ThreeNZ:IR)). rational. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)