proposition: Theorem EvenClosestMonotone : MonotoneP radix EvenClosest.
proof: Proof. red in |- *; simpl in |- *; intros p q p' q' H' H'0 H'1. apply (ClosestMonotone p q); auto; case H'0; case H'1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz