proposition: Lemma Pshiftl_nat_Zpower : forall n p, Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n.
proof: Proof. intros. rewrite Z.mul_comm. induction n. simpl; auto. transitivity (2 * (2 ^ Z.of_nat n * Zpos p)). rewrite <- IHn. auto. rewrite Z.mul_assoc. rewrite Nat2Z.inj_succ. rewrite <- Z.pow_succ_r; auto with zarith. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic