proposition: Theorem LSB_rep_min : forall p : float, exists z : Z, p = Float z (LSB p) :>R.
proof: Proof. intros p; exists (Zquotient (Fnum p) (Zpower_nat radix (Z.abs_nat (LSB p - Fexp p)))). unfold FtoRradix, FtoR, LSB in |- *; simpl in |- *. rewrite powerRZ_add; auto with real zarith. 2: apply IZR_neq; lia. rewrite <- Rmult_assoc. replace (maxDiv (Fnum p) (Fdigit radix p) + Fexp p - Fexp p)%Z with (Z_of_nat (maxDiv (Fnum p) (Fdigit radix p))); auto. rewrite Zabs2Nat.id. rewrite <- Zpower_nat_Z_powerRZ; auto with zarith. rewrite <- mult_IZR. rewrite <- ZdividesZquotient; auto with zarith. now apply sym_not_eq, Z.lt_neq, Zpower_nat_less. apply maxDivCorrect. ring. Qed.
imports: Reals ZArith List PeanoNat Psatz