fact: Definition change_le_func a := match a with | raLe x y => match get_float2_bound x with | reFloat2 _ _ as x => raBound (Some x) y None | _ => match get_float2_bound y with | reFloat2 _ _ as y => raBound None x (Some y) | _ => a end end | _ => a end.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library