proposition: Theorem neg : forall x : R, forall xi zi : FF, BND x xi -> neg_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). rewrite Fopp2_correct. clear H2. intro H2. apply IRopp with (1 := H1) (2 := H2) (3 := Hx). Qed.
imports: Gappa_common Gappa_decimal