proposition: Lemma Rnat_ltP x y : reflect (x < y)%num (spec_N x < spec_N y).
proof: Proof. by apply: (iffP idP); rewrite -Rnat_ltE /lt_op /lt_N; apply N.ltb_lt. Qed.
imports: ZArith Lia mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements pos)