add assumption

Author: thanhnguyen-aws

library/core/src/num/dec2flt/decimal_seq.rs

@@ -159,6 +159,8 @@ impl DecimalSeq {
 
         #[safety::loop_invariant(self.num_digits <= Self::MAX_DIGITS && self.decimal_point <= self.num_digits as i32)]
         while n > 0 {
+            //true but hard to write proof with kani currently
+            kani::assume(write_index > 0);
             write_index -= 1;
             let quotient = n / 10;
             let remainder = n - (10 * quotient);