proposition: Lemma int_ind_bounded : forall (P : int -> Prop) min max, min <=? max = true -> P min -> (forall i, min <=? i = true -> i <? max = true -> P i -> P (i + 1)) -> P max.
proof: Proof. intros P min max Hle Hmin Hrec. rewrite leb_spec in Hle. assert (Bmin := to_Z_bounded min);assert (Bmax := to_Z_bounded max). replace max with (min + (max - min)) by ring. generalize (leb_refl (max - min)). pattern (max - min) at 1 3. apply int_ind. intros _; replace (min + 0) with min by ring; exact Hmin. intros i Hi1 IH; revert Hi1. rewrite ltb_spec, leb_spec. assert (Bi := to_Z_bounded i). rewrite max_int_wB; intro Hi1. replace (min + (i + 1)) with (min + i + 1) by ring. rewrite to_Z_add_1_wB, sub_spec, Z.mod_small by lia. intro Hi2; apply Hrec. rewrite leb_spec, add_spec, Z.mod_small; lia. rewrite ltb_spec, add_spec, Z.mod_small; lia. apply IH. rewrite leb_spec, sub_spec, Z.mod_small; lia. Qed.
imports: Bool List PArray Int63 Ring63 ZArith Psatz