proposition: Lemma pos_le_mul : forall p q , (p <= p * q)%positive.
proof: Proof. intros p q; replace p with (p * 1)%positive at 1 by ( now rewrite Pos.mul_1_r). apply Pos.mul_le_mono_l; apply Pos.le_1_l. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)