proposition: Lemma FtoR_mul : forall beta s1 s2 m1 m2 e1 e2, (FtoR beta s1 m1 e1 * FtoR beta s2 m2 e2)%R = FtoR beta (xorb s1 s2) (m1 * m2) (e1 + e2).
proof: Proof. intros beta s1 s2 m1 m2 e1 e2. rewrite 3!FtoR_split. unfold F2R. simpl. rewrite bpow_plus. case s1 ; case s2 ; simpl ; rewrite <- Rmult_assoc, (Rmult_comm (IZR _)), (Rmult_assoc _ _ (IZR _)), <- mult_IZR ; simpl ; ring. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic