feat: getLsb_signExtend

[bollu]

This proof needs cleanup, and is stacked over the theory developed over at #4179 . The key idea is to notice that signExtend behavior is controlled by the msb. When msb = false, sext behaves the same as trunc. When msb = true, sext behaves like trunc but adds high 1-bits. This is expressed using the negate-truncate-negate pattern. Lemma statements below:

theorem signExtend_eq_neg_truncate_neg_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
    (x.signExtend v) = x.truncate v := by

theorem signExtend_eq_neg_truncate_neg_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
    (x.signExtend v) = ~~~((~~~x).truncate v) := by

These give the final theorem statement:

theorem getLsb_signExtend {x  : BitVec w} {v i : Nat} :
    (x.signExtend v).getLsb i = (decide (i < v) && if i < w then x.getLsb i else x.msb) := by