proposition: Lemma sub_refl : forall x : R, forall zi : FF, contains_zero_helper zi = true -> BND (x - x) zi.
proof: Proof. intros x zi Hb. unfold Rminus. rewrite (Rplus_opp_r x). apply contains_zero with (1 := Hb). Qed.
imports: Gappa_common Gappa_decimal