proposition: Lemma N_le_mul_pos : forall q p, (q <= q * N.pos p)%N.
proof: Proof. intros q p; replace q with (q * 1)%N at 1. apply N.mul_le_mono_nonneg_l. apply N_0_le_n. destruct p;discriminate. rewrite N.mul_1_r; auto. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)