proposition: Lemma average_no_underflow: (bpow emin) <= Rabs a -> av <> 0.
proof: Proof. Proof with auto with typeclass_instances. unfold av,a,average. case (Rle_bool_spec 0 x); case (Rle_bool_spec 0 y); intros. case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_no_underflow... apply avg_half_sub_no_underflow... now rewrite Rplus_comm. apply avg_naive_no_underflow... apply avg_naive_no_underflow... case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_no_underflow... right; split; now left. apply avg_half_sub_no_underflow... right; split; now left. now rewrite Rplus_comm. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)