proposition: Theorem constant10 : forall x : float10, forall zi : FF, constant10_helper x zi = true -> BND x zi.
proof: Proof. intros x zi Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Dle_fd_correct _ _ H1). clear H1. intro H1. generalize (Dle_df_correct _ _ H2). clear H2. intro H2. split ; assumption. Qed.
imports: Gappa_common Gappa_decimal