proposition: Lemma shift_correct : forall beta m e, Zpos (shift beta m e) = (Zpos m * Zpower_pos beta e)%Z.
proof: Proof. intros beta m e. rewrite Z.pow_pos_fold. unfold shift. set (r := match radix_val beta with Zpos r => r | _ => xH end). rewrite iter_pos_nat. rewrite Zpower_Zpower_nat by easy. simpl Z.abs_nat. induction (nat_of_P e). simpl. now rewrite Pmult_comm. rewrite iter_nat_S, Zpower_nat_S. rewrite Zpos_mult_morphism. rewrite IHn. replace (Zpos r) with (radix_val beta). ring. unfold r. generalize (radix_val beta) (radix_prop beta). clear. now intros [|p|p]. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic