proposition: Lemma mag_1 : mag 1 = 1%Z :> Z.
proof: Proof. apply mag_unique_pos; rewrite bpow_1; simpl; split; [now right|apply IZR_lt]. assert (H := Zle_bool_imp_le _ _ (radix_prop r)); revert H. now apply Z.lt_le_trans. Qed.
imports: Coq(Psatz Reals ZArith) Zaux