proposition: Lemma map_spec_N_inj : injective (map spec_N).
proof: Proof. apply inj_map => m n Hmn. rewrite -(nat_of_binK m) -(nat_of_binK n). by rewrite /spec_N in Hmn; rewrite Hmn. 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)