proposition: Lemma signExtend_fromNat extra n m : m < 2^n -> signExtend extra (fromNat (n:=n.+1) m) = #m.
proof: Proof. move => LT. unfold signExtend. rewrite -splitmsb_msb. rewrite splitmsb_fromNat. simpl. rewrite divn_small => //. simpl. replace (copy extra false ## (fromNat (n:=n.+1) m)) with (zeroExtend extra (fromNat (n:=n.+1) m)). apply zeroExtend_fromNat. rewrite expnS. apply: (ltn_trans LT). apply ltn_Pmull => //. apply expn_gt0. done. 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