proposition: Theorem isMaxComp : forall (r1 r2 : R) (min max : float), isMin b radix r1 min -> isMax b radix r1 max -> (min < r2)%R -> (r2 < max)%R -> isMax b radix r2 max.
proof: Proof. intros r1 r2 min max H' H'0 H'1 H'2; split. case H'0; auto. split. apply Rlt_le; auto. intros f H'3 H'4. case H'0; auto. intros H'5 H'6; elim H'6; intros H'7 H'8; apply H'8; clear H'6; auto. case (Rle_or_lt r1 (FtoR radix f)); auto; intros C1. absurd (min < FtoR radix f)%R. apply Rle_not_lt. case H'. intros H'6 H'9; elim H'9; intros H'10 H'11; apply H'11; clear H'9; auto. apply Rlt_le; auto. apply Rlt_le_trans with (1 := H'1); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz