proposition: Lemma fromNatBounded_eq m1 m2 n : m1 < 2^n -> m2 < 2^n -> (m1==m2) = (fromNat (n:=n) m1 == fromNat m2).
proof: Proof. move => B1 B2. case E: (m1 == m2); case E': (#m1 == #m2) => //. by rewrite (eqP E) eq_refl in E'. rewrite -(toNat_fromNatBounded B1) -(toNat_fromNatBounded B2) in E. by rewrite (eqP E') eq_refl in E. Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec