proposition: Theorem get_height_correct: forall digits N, Zpos N <= Zpos digits * (2 ^ (Zpos (get_height digits N) -1)).
proof: Proof. intros digits N. unfold get_height. assert (H1 := Pdiv_le N digits). case_eq (is_one (Pdiv N digits)); intros H2. rewrite (is_one_one _ H2) in H1. rewrite Z.mul_1_r in H1. change (2^(1-1))%Z with 1; rewrite Z.mul_1_r; auto. clear H2. apply Z.le_trans with (1 := H1). apply Z.mul_le_mono_nonneg_l. auto with zarith. rewrite Pos2Z.inj_succ; unfold Z.succ. rewrite Z.add_comm; rewrite Z.add_simpl_l. apply plength_pred_correct. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic