proposition: Theorem subset_l : forall x : R, forall xi : FF, forall f : float2, BND x xi -> Fle2 f (lower xi) = true -> (f <= x)%R.
proof: Proof. intros x xi f Hx Hb. generalize (Fle2_correct _ _ Hb). clear Hb. intro H1. apply Rle_trans with (1 := H1). exact (proj1 Hx). Qed.
imports: Gappa_common Gappa_decimal