proposition: Lemma Pos2Nat_le_n_pn : forall p q, (Pos.to_nat p <= Pos.to_nat p * Pos.to_nat q)%nat.
proof: Proof. intros p q; replace (Pos.to_nat p * Pos.to_nat q)%nat with (Pos.to_nat (p * q)) by (now rewrite Pos2Nat.inj_mul). apply Pos2Nat.inj_le; apply pos_le_mul. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)