fact: Definition clean_pow_func t := match t with | reBpow2 x => reFloat2 1 x | reBpow10 x => reFloat10 1 x | rePow2 x => reFloat2 1 x | rePow10 x => reFloat10 1 x | _ => t end.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library