proposition: Lemma Pos_to_nat_neq_0 : forall p, Pos.to_nat p <> 0%nat.
proof: Proof. induction p; cbn. discriminate. rewrite Pos2Nat.inj_xO. simpl; lia. discriminate. Qed.
imports: Coq(Arith NArith Lia Recdef) additions(Pow Compatibility Wf_transparent)