proposition: Theorem union' : forall (x : R) (xi : FF) (P : Prop), (BND x xi -> P) -> (Rle (upper xi) x -> P) -> Rle (lower xi) x -> P.
proof: Proof. intros x xi P H1 H2 Hx. destruct (Rlt_le_dec x (upper xi)) as [H|H]. apply H1. apply (conj Hx). now apply Rlt_le. now apply H2. Qed.
imports: Gappa_common Gappa_decimal