proposition: Lemma signExtendK extra n : pcancel (@signExtend extra n) (signTruncate extra).
proof: Proof. move => p. rewrite /signExtend /signTruncate split2app. case: (msb p). + by rewrite /ones eq_refl. + by rewrite /zero eq_refl. 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