fact: Definition round_round_eq fexp1 fexp2 choice1 choice2 x := round beta fexp1 (Znearest choice1) (round beta fexp2 (Znearest choice2) x) = round beta fexp1 (Znearest choice1) x.
imports: Coq(ZArith Reals Psatz) Core FTZ