fact: Definition eqExprTypePrim {T} (e1 : evalExprTypePrim T) (e2 : evalExprTypeRounded T) := convertiblePrim e1 /\ isConversionPrim e1 e2.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)