proposition: Lemma signTruncateK extra n p q : signTruncate extra (n:=n) p = Some q -> signExtend extra (n:=n) q = p.
proof: Proof. rewrite /signTruncate/signExtend. rewrite (split2eta p) split2app. case P: (_ || _) => // H. have EQ: low n.+1 p = q by congruence. subst. case M: (msb _). + rewrite M andTb andFb orbF in P. by rewrite (eqP P). + rewrite M andTb andFb orFb in P. by rewrite (eqP P). 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