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

Author: tautschnig

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

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