proposition: Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n.
proof: Proof. intros p n. rewrite Pmult_nat_mult. apply Nat.le_trans with (1*n). - now rewrite Nat.mul_1_l. - apply Nat.mul_le_mono_r. apply Pos2Nat.is_pos. Qed.
imports: BinPos PeanoNat