proposition: Theorem invert_abs : forall x : R, forall xi zi : FF, BND (Rabs x) xi -> invert_abs_helper xi zi = true -> BND x zi.
proof: Proof. intros x xi zi Hx Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). rewrite Fopp2_correct. clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. split. apply Rle_trans with (1 := H1). apply Ropp_le_cancel. rewrite Ropp_involutive. apply Rle_trans with (2 := proj2 Hx). pattern x at 2 ; rewrite <- Ropp_involutive. rewrite Rabs_Ropp. apply Rabs_idem. apply Rle_trans with (2 := H2). apply Rle_trans with (1 := Rabs_idem x) (2 := proj2 Hx). Qed.
imports: Gappa_common Gappa_decimal