proposition: Theorem of_pos_correct: forall p, Zpos p < base digits -> [|(snd (of_pos p))|] = Zpos p.
proof: Proof. intros p Hp. generalize (spec_of_pos p). case (of_pos p); intros n w1; simpl. case n; auto with zarith. intros p1 Hp1; contradict Hp; apply Z.le_ngt. replace (base digits) with (1 * base digits + 0) by ring. rewrite Hp1. apply Z.add_le_mono. - apply Z.mul_le_mono_nonneg. 1-2, 4: lia. unfold base; auto with zarith. - case (spec_to_Z w1); auto with zarith. Qed.
imports: ZArith Lia Znumtheory Zpow_facts DoubleType