proposition: Lemma avg_half_sub_no_underflow: (0 <= x /\ 0 <= y) \/ (x <= 0 /\ y <= 0) -> (bpow emin) <= Rabs a -> av <> 0.
proof: Proof. Proof with auto with typeclass_instances. intros; now apply avg_half_sub_no_underflow_aux3. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)