proposition: Lemma Zlt_le_eq_S : forall x y : Z, (x < y)%Z -> (y <= x + 1)%Z -> y = (x + 1)%Z.
proof: Proof. intros. case (Z_le_lt_eq_dec y (x + 1) H0). intro H1. apply False_ind. generalize (Zlt_le_succ x y H). intro. apply (Zlt_not_le y (x + 1) H1). replace (x + 1)%Z with (Z.succ x). assumption. reflexivity. trivial. Qed.
imports: Coq(Lia)