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