proposition: Theorem isMinComp : forall (r1 r2 : R) (min max : float), isMin b radix r1 min -> isMax b radix r1 max -> (min < r2)%R -> (r2 < max)%R -> isMin b radix r2 min.
proof: Proof. intros r1 r2 min max H' H'0 H'1 H'2; split. case H'; auto. split. apply Rlt_le; auto. intros f H'3 H'4. case H'; 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 (FtoR radix f) r1); auto; intros C1. absurd (FtoR radix f < max)%R. apply Rle_not_lt. case H'0. 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 Rle_lt_trans with (2 := H'2); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz