proposition: Lemma add_exact_correct : forall x y, toX (add_exact x y) = Xadd (toX x) (toX y).
proof: Proof. intros x y. unfold toX. rewrite <- Fadd_exact_correct. destruct x as [|mx ex]. apply refl_equal. destruct y as [|my ey]. simpl. now case (mantissa_sign mx). simpl. generalize (mantissa_sign_correct mx). case_eq (mantissa_sign mx). simpl. now case (mantissa_sign my). intros sx px Hx (Hx1, Hx2). generalize (mantissa_sign_correct my). case (mantissa_sign my). simpl. now rewrite Hx. intros sy py (Hy1, Hy2). unfold Fadd_exact, Fadd_slow_aux. now apply add_exact_aux_correct. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig