proposition: Lemma mul_correct : forall mode p x y, toX (mul mode p x y) = Xround radix mode (prec p) (Xmul (toX x) (toX y)).
proof: Proof. intros mode p x y. unfold toX. rewrite <- Fmul_correct. destruct x as [|mx ex] ; destruct y as [|my ey] ; try easy. simpl. now case (mantissa_sign mx). simpl. generalize (mantissa_sign_correct mx). case_eq (mantissa_sign mx). simpl. intros. rewrite H. now case (mantissa_sign my). intros sx px Hx (Hx1, Hx2). rewrite (match_helper_1 _ _ (fun s py => round_aux mode p (Datatypes.xorb sx s) (mantissa_mul px py) (exponent_add ex ey) pos_Eq) (fun a => FtoX (toF a))). rewrite (match_helper_1 _ _ (fun s p => Basic.Float s (MtoP p) (EtoZ ey)) (fun a => FtoX (Fmul mode (prec p) (Basic.Float sx (MtoP px) (EtoZ ex)) a))). simpl. generalize (mantissa_sign_correct my). case (mantissa_sign my). trivial. intros sy py (_, Hy2). destruct (mantissa_mul_correct px py) as (H1, H2) ; try assumption. rewrite round_aux_correct. rewrite H1. clear H1. rewrite exponent_add_correct. apply refl_equal. exact H2. Qed.
imports: Coq(ZArith Reals Lia Bool Psatz) Flocq(Zaux Raux Digits Bracket) mathcomp.ssreflect(ssrbool) Xreal Basic Generic Generic_proof Sig Specific_sig