proposition: Lemma mag_minus1 : forall z, z <> 0%R -> (mag beta z - 1)%Z = mag beta (z / IZR beta).
proof: Proof. intros z Hz. unfold Zminus. rewrite <- mag_mult_bpow by easy. now rewrite bpow_opp, bpow_1. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative