proposition: Lemma implem_NK : cancel implem_N spec_N.
proof: Proof. move=> n; symmetry; apply refinesP. have{1}->: n = spec_id (implem_id n) by []. refines_apply. 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)