proposition: Lemma subnormal_1: bpow (emin+prec-1) < M -> bpow (emin+prec-1) < Rabs (round_flt (round_flt (t1*t2)*t3)).
proof: Proof. Proof with auto with typeclass_instances. intros H. apply subnormal_aux with t4. apply generic_format_round... rewrite 2!Rabs_right. intros Y. case (Rle_or_lt (round_flt (t1 * t2)) 1); intros Y1. apply subnormal_aux_aux in Y1. apply Rle_trans with (2:=Y1). apply t4Let3. case (Rle_or_lt t3 1); intros Y2. apply Rle_trans with (2:=Y2). apply t4Let3. contradict Y. apply Rlt_not_le. apply Rlt_le_trans with (1:=Y1). apply round_ge_generic... apply generic_format_round... rewrite <- (Rmult_1_r (round_flt (t1 * t2))) at 1. apply Rmult_le_compat_l. apply FLT_pos_is_pos. apply Rmult_le_pos. apply t1pos_. apply t2pos_. now left. apply Rle_ge, t4pos_. apply Rle_ge, FLT_pos_is_pos. apply Rmult_le_pos. apply FLT_pos_is_pos. apply Rmult_le_pos. apply t1pos_. apply t2pos_. apply t3pos_. rewrite Rabs_right. exact H. apply Rle_ge, Mpos_. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)