proposition: Lemma is_int n : 0 <= n < 2 ^ φ digits → n = φ (of_Z n).
proof: Proof. destruct n;[reflexivity | | lia ]. intros [_ h]. simpl. unfold of_pos. rewrite of_pos_rec_spec by lia. symmetry; apply Z.mod_small. split. - lia. - exact h. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63