proposition: Lemma gen_float_prop : stable_expr gen_float_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. destruct o ; try apply refl_equal. destruct x ; try apply refl_equal. destruct z ; apply refl_equal. destruct o ; try apply refl_equal ; destruct x ; try apply refl_equal ; destruct y ; try apply refl_equal. apply compact_posfloat2_correct. apply compact_posfloat10_correct. simpl. rewrite <- (bpow_powerRZ radix2). apply compact_posfloat2_correct. simpl. rewrite <- (bpow_powerRZ radix10). apply compact_posfloat10_correct. destruct z0 ; try apply refl_equal. generalize (float2_of_pos_correct p). simpl. destruct (float2_of_pos p) as ([|[m|m|]|m], [|e|e]) ; intros H ; try apply refl_equal. rewrite compact_posfloat2_correct. rewrite <- H. unfold float2R, F2R. simpl. now rewrite Rmult_1_l. simpl. rewrite <- positive_nat_Z. apply sym_eq, INR_IZR_INZ. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library