proposition: Lemma zeroExtend_fromNat extra n m : m < 2^n -> zeroExtend extra (fromNat (n:=n) m) = #m.
proof: Proof. move => LT. apply toNat_inj. rewrite toNat_zeroExtend. rewrite toNat_fromNatBounded => //. rewrite toNat_fromNatBounded => //. rewrite expnD. apply (leq_trans LT). apply leq_pmulr. apply expn_gt0. 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