fact: Fixpoint C2M_list {Tl} : evalExprTypeFloat_list Tl -> evalExprTypeRounded_list Tl := match Tl with | nil => fun l => tt | _ :: _ => fun l => (C2M (fst l), C2M_list (snd l)) end.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)