proposition: Lemma avg_naive_no_underflow: (bpow emin) <= Rabs a -> av <> 0.
proof: Proof. Proof with auto with typeclass_instances. intros H. cut (bpow emin <= Rabs av). intros H1 H2. rewrite H2 in H1; rewrite Rabs_R0 in H1. contradict H1. apply Rlt_not_le. apply bpow_gt_0. rewrite avg_naive_correct. apply abs_round_ge_generic... apply generic_format_FLT_bpow... lia. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)