fact: Fixpoint list_var_aux n init := match n with | O => nil | S n' => CVar init :: list_var_aux n' (S init) end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr