proposition: Lemma bin_of_natE : bin_of_nat =1 N.of_nat.
proof: Proof. move=> n. by rewrite -[bin_of_nat n]nat_of_binK bin_of_natK. 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)