proposition: Lemma uint2N_pred n : n <> 0%int63 -> uint2N n = (uint2N (Uint63.pred n)).+1.
proof: Proof. move=> Hn. rewrite /uint2N Uint63.pred_spec. case HnZ: (Uint63.to_Z n) => [|m|m]. - rewrite (_ : 0 = Uint63.to_Z 0)%Z // in HnZ. move/Uint63.to_Z_inj in HnZ. by elim Hn. - have Hm1 : (0 <= Z.pos m - 1 < Uint63.wB)%Z. split. by apply leZsub1, Pos2Z.is_pos. apply (Z.lt_trans _ (Z.pos m)). by apply leZsub1, Z.le_refl. rewrite -HnZ; by apply uint63_max. rewrite Zmod_small //. case HmZ: (Z.pos m - 1)%Z => [|p|p]. + by move/Z.sub_move_r: HmZ => /= [] ->. + apply Nat2Z.inj => /=. rewrite positive_nat_Z Pos2SuccNat.id_succ Pos2Z.inj_succ -HmZ. by rewrite (Z.succ_pred (Z.pos m)). + by destruct m. - move: (uint63_min n). rewrite HnZ => /Zle_not_lt; elim. by apply Zlt_neg_0. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63