proposition: Lemma Rnat_eqxx (c : N) : (c == c)%C.
proof: Proof. by rewrite Rnat_eqE. 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)