proposition: Lemma adjust_mantissa_Eq mode b p : adjust_mantissa mode p pos_Eq b = p.
proof: Proof. now destruct mode. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic