proposition: Remark Pos_to_nat_diff_0 n : Pos.to_nat n <> 0%nat.
proof: Proof. rewrite Nat.neq_0_lt_0; apply Pos2Nat.is_pos. Qed.
imports: Coq(List PArith Relations Lia) additions(Monoid_def Monoid_instances Strategies) Coq(Recdef Wf_nat) additions(More_on_positive Pow Euclidean_Chains Dichotomy BinaryStrat) Coq(NArith)