proposition: Lemma Rnat_leE (c d : N) : (c <= d)%C = (spec_N c <= spec_N d)%N.
proof: Proof. symmetry; eapply refines_eq. refines_apply. refines_abstr. 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)