proposition: Theorem MaxCompatible : CompatibleP (isMax b radix).
proof: Proof. red in |- *. intros r1 r2 p q H' H'0 H'1 H'2; split; auto. rewrite <- H'0; unfold FtoRradix in H'1; rewrite <- H'1; case H'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz