proposition: Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
proof: Proof. induction 1 as [|* [|]]; auto. - intros Hle; exfalso; apply (Nat.nle_succ_diag_l _ Hle). - intros Hle; inversion Hle; constructor; auto. Qed.
imports: PeanoNat