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