proposition: Lemma get_float2_bound_correct : stable_expr get_float2_bound.
proof: Proof. intros b. unfold get_float2_bound. rewrite (transform_expr_correct _ merge_float2_prop). rewrite (transform_expr_correct _ clean_pow_prop). rewrite (transform_expr_correct _ gen_float_prop). now rewrite (transform_expr_correct _ remove_inv_prop). Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library