proposition: Lemma change_abs_prop : stable_atom change_abs_func.
proof: Proof. intros [l v u|x y l u|v w|v w|f x|f x] ; try easy. destruct v as [x|x|x y|x y|o x|o x y|x|x|x|x|x|x|f m x] ; try easy. destruct o ; try easy. split. now intros (_,H). split. replace (convert_expr (reFloat2 0 0)) with R0. apply Rabs_pos. apply eq_sym, Rmult_0_l. exact H. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library