proposition: Lemma change_le_prop : stable_atom change_le_func.
proof: Proof. intros [l v u|x y l u|v w|v w|f x|f x] ; try easy. simpl. assert (Hv := get_float2_bound_correct v). assert (Hw := get_float2_bound_correct w). destruct (get_float2_bound v) as [x|x|x y|x y|o x|o x y|x|x|x|x|x|x|f m x] ; destruct (get_float2_bound w) as [x'|x'|x' y'|x' y'|o' x'|o' x' y'|x'|x'|x'|x'|x'|x'|f' m' x'] ; try easy ; try (now rewrite <- Hw) ; now rewrite <- Hv. Qed.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library