proposition: Lemma clean_pow_prop : stable_expr clean_pow_func.
proof: Proof. intros [x|x|x y|x y|o x|o x y|x|x|x|x|x|x|f m x] ; try apply refl_equal. apply (F2R_bpow radix2 x). apply (F2R_bpow radix10 x). simpl. unfold float2R. rewrite F2R_bpow. apply bpow_powerRZ. simpl. unfold float10R. rewrite F2R_bpow. apply bpow_powerRZ. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library