proposition: Lemma p3m_pos : forall i : nat, [0] [<] p3m i.
proof: Proof. intros. unfold p3m in |- *. apply nexp_resp_pos. apply div_resp_pos. apply pos_three. apply pos_one. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)