proposition: Lemma match_helper_1 : forall A B y2, forall f : A -> B, forall x y1, f (match mantissa_sign x with Mzero => y1 | Mnumber s p => y2 s p end) = match mantissa_sign x with Mzero => f y1 | Mnumber s p => f (y2 s p) end.
proof: Proof. intros. now case (mantissa_sign x). Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig