proposition: Theorem FmaxRep : forall p q : float, isMax p q -> exists m : Z, q = Float m (Fexp p) :>R.
proof: Proof. intros p q H'; case (FminRep (Fopp p) (Fopp q)). unfold FtoRradix in |- *; rewrite Fopp_correct. apply MaxOppMin; auto. intros x H'0. exists (- x)%Z. rewrite <- (Ropp_involutive (FtoRradix q)). unfold FtoRradix in |- *; rewrite <- Fopp_correct. unfold FtoRradix in H'0; rewrite H'0. unfold FtoR in |- *; simpl in |- *; auto with real. rewrite Ropp_Ropp_IZR; rewrite Ropp_mult_distr_l_reverse; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz