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 Zmult_1_r in H1. change (2^(1-1))%Z with 1; rewrite Zmult_1_r; auto. clear H2. apply Z.le_trans with (1 := H1). apply Zmult_le_compat_l; auto with zarith. rewrite Zpos_succ_morphism; unfold Z.succ. rewrite Zplus_comm; rewrite Zminus_plus. apply plength_pred_correct. Qed.
imports: ZArith Zpow_facts