proposition: Lemma shift1_correct r e : shift r 1 e = (Z.to_pos r ^ e)%positive.
proof: Proof. generalize (shift_correct r 1 e). rewrite Zmult_1_l, <-(radix_to_pos r) at 1. rewrite <-Pos2Z.inj_pow_pos. now intro H; injection H. Qed.
imports: Coq(Reals Bool ZArith Psatz) Flocq(Core Digits Bracket Round Operations) mathcomp.ssreflect(ssrbool) Stdlib Xreal Basic Generic