proposition: Theorem EvenClosestCompatible : CompatibleP b radix EvenClosest.
proof: Proof. red in |- *; simpl in |- *. intros r1 r2 p q H' H'0 H'1 H'2; red in |- *. inversion H'. split. apply (ClosestCompatible r1 r2 p q); auto. case H0; intros H1. left. apply FNevenEq with (f1 := p); auto. case H; auto. right; intros q0 H'3. unfold FtoRradix in |- *; rewrite <- H'1; auto. apply H1; auto. apply (ClosestCompatible r2 r1 q0 q0); auto. case H'3; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz