proposition: Lemma length_list_var_aux : forall n i, length (list_var_aux n i) = n.
proof: Proof. now induction n; [| intros i; simpl; rewrite (IHn (S i))]. 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