proposition: Lemma subnormal_2: bpow (emin+prec-1) < M -> bpow (emin+prec-1) < Rabs (round_flt (t1*t2)).
proof: Proof. Proof with auto with typeclass_instances. intros H. apply subnormal_aux with t3. apply generic_format_round... rewrite 2!Rabs_right. apply subnormal_aux_aux. apply Rle_ge, t3pos_. apply Rle_ge, FLT_pos_is_pos. apply Rmult_le_pos. apply t1pos_. apply t2pos_. apply subnormal_1. exact H. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)