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