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