proposition: Lemma subnormal_aux: forall x y, format x -> (Rabs x <= 1 -> Rabs y <= 1) -> bpow (emin+prec-1) < Rabs (round_flt (x*y)) -> bpow (emin+prec-1) < Rabs x.
proof: Proof. Proof with auto with typeclass_instances. intros x y Fx H1 H2. case (Rle_or_lt (Rabs x) (bpow (emin + prec - 1))); intros H3;[idtac|assumption]. contradict H2. apply Rle_not_lt. apply Rle_trans with (2:=H3). assert (H4: format (round_flt (x * y))). apply generic_format_round... rewrite <- round_NE_abs... apply round_le_generic... now apply generic_format_abs. rewrite <- (Rmult_1_r (Rabs x)), Rabs_mult. apply Rmult_le_compat_l. apply Rabs_pos. apply H1. apply Rle_trans with (1:=H3). apply Rle_trans with (bpow 0). apply bpow_le. lia. now apply Rle_refl. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)