proposition: Lemma nth_list_var_aux_S: forall n k i t, nth (S n) (list_var_aux (S k) i) (Psucc t) = Psucc (nth n (list_var_aux k i) t).
proof: Proof. induction n; destruct k; [easy.. |]. intros i t. simpl in *. now rewrite (IHn k (S i) t). Qed.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr