proposition: Lemma p3m_mon' : forall i j : nat, i <= j -> p3m j [<=] p3m i.
proof: Proof. intros. unfold p3m in |- *. apply small_nexp_resp_le; try apply less_leEq; algebra. Qed.
imports: Coq.ZArith.ZArith Coq.Arith.Compare CoRN.reals.NRootIR Coq(Lia)