fact: Definition signTruncate extra {n} (p: BITS (n.+1 + extra)) : option (BITS n.+1) := let (hi,lo) := split2 extra _ p in if msb lo && (hi == ones _) || negb (msb lo) && (hi == zero _) then Some lo else None.
imports: Coq(ZArith.ZArith Strings.String) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp)