proposition: Lemma change_format_prop : stable_atom_tree change_format_func.
proof: Proof. unfold change_format_func. intros [l v u|x y l u|v w|v w|[em|em [|p|p]|[|p|p]] x|[em|em [|p|p]|[|p|p]] x] pos ; try (case pos ; easy) ; simpl ; intros H. destruct pos ; simpl. apply sym_eq, round_generic. apply valid_rnd_N. exact H. contradict H. rewrite <- H. apply generic_format_round. apply FIX_exp_valid. apply valid_rnd_N. destruct pos ; simpl. apply sym_eq, round_generic. apply valid_rnd_N. exact H. contradict H. rewrite <- H. apply generic_format_round. now apply FLT_exp_valid. apply valid_rnd_N. destruct pos ; simpl. apply sym_eq, round_generic. apply valid_rnd_N. exact H. contradict H. rewrite <- H. apply generic_format_round. now apply FLX_exp_valid. apply valid_rnd_N. destruct pos ; simpl. apply sym_eq, round_generic. apply valid_rnd_N. now apply generic_format_FIX. contradict H. rewrite <- H. apply FIX_format_generic. apply generic_format_round. apply FIX_exp_valid. apply valid_rnd_N. destruct pos ; simpl. apply sym_eq, round_generic. apply valid_rnd_N. apply generic_format_FLT. exact H. contradict H. rewrite <- H. apply FLT_format_generic. easy. apply generic_format_round. now apply FLT_exp_valid. apply valid_rnd_N. destruct pos ; simpl. apply sym_eq, round_generic. apply valid_rnd_N. apply generic_format_FLX. exact H. contradict H. rewrite <- H. apply FLX_format_generic. easy. apply generic_format_round. now apply FLX_exp_valid. apply valid_rnd_N. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library