proposition: Lemma pos_lt_mul : forall p q , (1 < q -> p < p * q)%positive.
proof: Proof. intros p q H; replace p with (p * 1)%positive at 1 by ( now rewrite Pos.mul_1_r). apply Pos.mul_lt_mono_l; auto. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)