proposition: Lemma subnormal_aux_aux: (round_flt (t1 * t2)) <= 1 -> t3 <= 1.
proof: Proof. Proof with auto with typeclass_instances. intros Y. case (Rle_or_lt t1 1); intros Y1. apply Rle_trans with (2:=Y1). apply Rle_trans with (1:=t3Let2). apply t2Let1. case (Rle_or_lt t2 1); intros Y2. apply Rle_trans with (2:=Y2). apply t3Let2. 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 t1) at 1. apply Rmult_le_compat_l. apply t1pos_. now left. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)