proposition: Lemma n2posK p : valid_pos p -> n2pos (pos2n p) = p.
proof: Proof. case: p => x y /andP[/= xLhw yLhw]; rewrite /pos2n /n2pos /= . have hw_gt0 : 0 < hw by apply: leq_ltn_trans xLhw. by rewrite divnMDl // modnMDl divn_small // addn0 modn_small. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)