RefinedC verification failed with code 1

Stdout:


Stderr:
Entering directory '/home/ec2-user/repo-2814'
      coqdep src/proofs/sum_upto/.refinedc.project.sum_upto.src.theory.d
        coqc src/proofs/sum_upto/generated_proof_main.{glob,vo}
        coqc src/proofs/sum_upto/my_lemmas.{glob,vo}
        coqc src/proofs/sum_upto/generated_code.{glob,vo}
        coqc src/proofs/sum_upto/generated_spec.{glob,vo}
File "src/proofs/sum_upto/dune", lines 2-5, characters 0-247:
2 | (coq.theory
3 |  (flags :standard -w -notation-incompatible-prefix -w -redundant-canonical-projection)
4 |  (name refinedc.project.sum_upto.src.sum_upto)
5 |  (theories Ltac2 RecordUpdate caesium iris lithium refinedc.typing refinedc.typing.automation stdpp))
        coqc src/proofs/sum_upto/generated_proof_sum_upto_n.{glob,vo} (exit 1)
Cannot solve side condition in function "sum_upto_n" !
Location: "src/sum_upto.c" [ 28 : 4 - 28 : 12 ]
Location: "src/sum_upto.c" [ 28 : 4 - 28 : 13 ]
up to date: true
Case distinction (if bool_decide (i ≤ n)) -> true
at "src/sum_upto.c" [ 27 : 9 - 27 : 15 ]
Goal:
n : nat
H : ((n * (n + 1)) `div` 2 ≤ max_int u32)
H0 : (n ≤ 1000)
i : nat
H1 : (i ≤ n + 1)
H2 : (min_int u32 ≤ i)
H3 : (i ≤ max_int u32)
H4 : (min_int u32 ≤ n)
H5 : (n ≤ max_int u32)
H6 : (i ≤ n)
H7 : (min_int u32 ≤ (i * (i - 1)) `div` 2)
H8 : ((i * (i - 1)) `div` 2 ≤ max_int u32)
---------------------------------------
((i * (i - 1)) `div` 2 + i ≤ max_int u32)


Cannot solve side condition in function "sum_upto_n" !
Location: "src/sum_upto.c" [ 30 : 2 - 30 : 13 ]
up to date: true
Case distinction (if bool_decide (i ≤ n)) -> false
at "src/sum_upto.c" [ 27 : 9 - 27 : 15 ]
Goal:
n : nat
H : ((n * (n + 1)) `div` 2 ≤ max_int u32)
H0 : (n ≤ 1000)
i : nat
H1 : (i ≤ n + 1)
H2 : (min_int u32 ≤ i)
H3 : (i ≤ max_int u32)
H4 : (min_int u32 ≤ n)
H5 : (n ≤ max_int u32)
H6 : (¬ i ≤ n)
---------------------------------------
((i * (i - 1)) `div` 2 = (n * (n + 1)) `div` 2)


File "./src/proofs/sum_upto/generated_proof_sum_upto_n.v", line 40, characters 2-6:
Error:  (in proof type_sum_upto_n): Attempt to save an incomplete proof
(the proof term is not complete because of given up (admitted) goals).
If this is really what you want to do, use Admitted in place of Qed.

Leaving directory '/home/ec2-user/repo-2814'
The call to [dune] returned with error code 1.