proposition: Lemma Ple_Zle_to_pos (z : Z) (p : positive) : (Z.to_pos z <= p)%positive <-> z <= Zpos p.
proof: Proof. destruct z as [| q | q]; simpl. + split; intros _; [apply Zle_0_pos | apply Pos.le_1_l]. + apply Ple_Zle. + split; intros _; [apply Zle_neg_pos | apply Pos.le_1_l]. Qed.
imports: Coq.ZArith.ZArith CoRN.stdlib_omissions.P Lia