proposition: Theorem ClosestCompatible : CompatibleP b radix Closest.
proof: Proof. red in |- *; simpl in |- *. intros r1 r2 p q H'; case H'. intros H'0 H'1 H'2 H'3 H'4. split; auto. intros f H'5. unfold FtoRradix in |- *; rewrite <- H'3; rewrite <- H'2; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz