proposition: Lemma between_in_int : forall k l, between k l -> forall r, in_int k l r -> P r.
proof: Proof. intro k; induction 1 as [|l]; intros r ?. - absurd (k < k). { apply Nat.lt_irrefl. } eapply in_int_lt; eassumption. - destruct (in_int_p_Sq k l r) as [| ->]; auto. Qed.
imports: PeanoNat