fact: Definition average (x y : R) := let samesign := match (Rle_bool 0 x), (Rle_bool 0 y) with true , true => true | false , false => true | _,_ => false end in if samesign then match (Rle_bool (Rabs x) (Rabs y)) with true => avg_half_sub emin prec x y | false => avg_half_sub emin prec y x end else avg_naive emin prec x y.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)