proposition: Lemma in_Zseq n a x : In x (Zseq a n) <-> (a <= x < a + Z.of_nat n).
proof: Proof. revert a. induction n; intros a. simpl. lia. split. - intros [ -> | h ]. lia. rewrite IHn in h. lia. - intros h. destruct (Z.eq_dec a x). now left. right. apply IHn. lia. Qed.
imports: Coq(ZArith Znumtheory Lia List Bool) Coqtail(Ztools Zpow)