proposition: Lemma not_zero_correct : forall z : R, forall zi : FF, BND z zi -> not_zero zi = true -> (z <> 0)%R.
proof: Proof. intros z zi Hz Hb. apply Rlt_dichotomy_converse. generalize (orb_prop _ _ Hb). clear Hb. intro H. elim H; clear H; intro H. right. generalize (Fpos_correct _ H). clear H. intro H. unfold Rgt. apply Rlt_le_trans with (1 := H). exact (proj1 Hz). left. generalize (Fneg_correct _ H). clear H. intro H. apply Rle_lt_trans with (2 := H). exact (proj2 Hz). Qed.
imports: Gappa_common Gappa_decimal