proposition: Lemma Ple_Zle (p q: positive): Pos.le p q <-> (Zpos p <= Zpos q).
proof: Proof. rewrite Ple_le, inj_le_iff. do 2 rewrite <- Zpos_eq_Z_of_nat_o_nat_of_P. reflexivity. Qed.
imports: Coq.ZArith.ZArith CoRN.stdlib_omissions.P Lia