proposition: Lemma Rord0_eq (n1 : nat) i i' : refines (@Rord0 n1) i i' -> i = i' :> nat.
proof: Proof. by rewrite refinesE =>->. Qed.
imports: ZArith NArith FMaps FMapAVL mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice finfun tuple fintype ssralg bigop) CoqEAL(hrel) CoqEAL(refinements) CoqEAL(param binord binnat) CoqEAL(seqmx ) CoqEAL(ssrcomplements) mathcomp.multinomials(mpoly freeg)