proposition: Lemma Ple_le (p q: positive): Pos.le p q <-> le (nat_of_P p) (nat_of_P q).
proof: Proof. rewrite Pos.le_lteq, Plt_lt, Nat.lt_eq_cases, nat_of_P_inj_iff. reflexivity. Qed.
imports: Coq.Setoids.Setoid Coq.PArith.BinPos Coq.PArith.Pnat ZArith_base