proposition: Lemma flt_1_aux : forall x y : R, forall yn : positive, FLT x 1 -> FLT y yn -> FLT (x * y)%R yn.
proof: Proof. intros x y yn [[mx ex] [<- Hx]] Hy. destruct mx as [|mx|mx]. rewrite float2_zero, Rmult_0_l. exists (Float2 Z0 0). split. apply float2_zero. now apply (Zpower_gt_0 radix2 (Zpos yn)). destruct mx ; try now destruct mx. destruct Hy as [[my ey] [<- Hy]]. exists (Float2 my (ex + ey)). split. 2: exact Hy. unfold float2R ; simpl. rewrite <- Operations.F2R_mult. unfold Operations.Fmult. now rewrite Zmult_1_l. destruct mx ; try now destruct mx. destruct Hy as [[my ey] [<- Hy]]. exists (Float2 (-my) (ex + ey)). split. 2: simpl ; now rewrite Zabs_Zopp. unfold float2R ; simpl. rewrite <- Operations.F2R_mult. unfold Operations.Fmult. now replace (-1 * my)%Z with (Z.opp my) by ring. Qed.
imports: Flocq(Core Sterbenz) Gappa_common Gappa_round_aux