proposition: Theorem match_FF2B : forall {T} fz fi fn ff x Hx, match FF2B x Hx return T with | B754_zero sx => fz sx | B754_infinity sx => fi sx | B754_nan b p _ => fn b p | B754_finite sx mx ex _ => ff sx mx ex end = match x with | F754_zero sx => fz sx | F754_infinity sx => fi sx | F754_nan b p => fn b p | F754_finite sx mx ex => ff sx mx ex end.
proof: Proof. now intros T fz fi fn ff [sx|sx|sx plx|sx mx ex] Hx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative BinarySingleNaN