proposition: Lemma int_ind : forall (P : int -> Prop), P 0 -> (forall i, (i <? max_int) = true -> P i -> P (i + 1)) -> forall i, P i.
proof: Proof. intros P HP0 Hrec i. assert (Bi := to_Z_bounded i). destruct Bi as [ Bi0 Bi ]. rewrite <- of_to_Z. rewrite Z2Nat.inj_lt in Bi; [ | exact Bi0 | lia ]; clear Bi0. rewrite <- (Z2Nat.id (to_Z i)); [ | apply to_Z_bounded ]. revert Bi. induction (Z.to_nat (to_Z i)); clear i. intro; apply HP0. rewrite Nat2Z.inj_lt. rewrite Z2Nat.id; [ | generalize wB_pos; clear IHn; lia ]. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_r. rewrite <- (Nat2Z.id n) in IHn at 1. rewrite <- Z2Nat.inj_lt in IHn; [ | clear IHn; lia | clear IHn; generalize wB_pos; lia ]. generalize (Z.of_nat n) IHn (Nat2Z.is_nonneg n); clear n IHn; intros z IHz Hz1 Hz2. replace (of_Z (z + 1)) with (of_Z z + 1). apply Hrec. apply ltb_spec. rewrite of_Z_spec, Z.mod_small, max_int_wB; lia. apply IHz; lia. apply to_Z_inj. rewrite of_Z_spec, Z.mod_small by lia. rewrite to_Z_add_1_wB, of_Z_spec. rewrite Z.mod_small; lia. rewrite of_Z_spec, Z.mod_small; lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz