proposition: Theorem constant1 : forall x : Z, forall zi : FF, constant2_helper (Float2 x 0) zi = true -> BND (Float1 x) zi.
proof: Proof. intros x zi Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). generalize (Fle2_correct _ _ H1). clear H1. intro H1. generalize (Fle2_correct _ _ H2). clear H2. intro H2. rewrite <- (Rmult_1_r (Float1 x)). change (Float1 x * 1)%R with (float2R (Float2 x 0)). split ; assumption. Qed.
imports: Gappa_common Gappa_decimal