proposition: Lemma contains_zero : forall zi : FF, contains_zero_helper zi = true -> BND 0 zi.
proof: Proof. intros zi Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fneg0_correct _ H1). clear H1. intro H1. generalize (Fpos0_correct _ H2). clear H2. intro H2. split ; assumption. Qed.
imports: Gappa_common Gappa_decimal