proposition: Lemma Pos2Nat_le_1_p : forall p, (1 <= Pos.to_nat p)%nat.
proof: Proof. intro p; change (Pos.to_nat 1 <= Pos.to_nat p)%nat; rewrite <- Pos2Nat.inj_le. apply Pos.le_1_l. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)