proposition: Lemma lt_O_positive_to_nat : forall (p : positive) (m : nat), 0 < m -> 0 < Pmult_nat p m.
proof: Proof. intro p. elim p. intros p0 H m H0. simpl in |- *. auto with arith. intros p0 H m H0. simpl in |- *. apply H. auto with arith. intros m H. simpl in |- *. assumption. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid