proposition: Lemma exists_lt : forall k l, exists_between k l -> k < l.
proof: Proof. Proof exists_le_S. #[local] Hint Immediate exists_le_S exists_lt: core. Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l. Proof. intros; apply le_S_n; auto. Qed.
imports: PeanoNat