proposition: Theorem union : forall (x : R) (xl : float2) (P : Prop), (Rle x xl -> P) -> (Rle xl x -> P) -> P.
proof: Proof. intros x xl P H1 H2. destruct (Rlt_le_dec x xl) as [H|H]. apply H1. now apply Rlt_le. now apply H2. Qed.
imports: Gappa_common Gappa_decimal