proposition: Lemma between_not_exists : forall k l, between k l -> (forall n:nat, in_int k l n -> P n -> ~ Q n) -> ~ exists_between k l.
proof: Proof. intro k; induction 1 as [|l]; red; intros. - absurd (k < k). { apply Nat.lt_irrefl. } auto. - absurd (Q l). { auto. } destruct (exists_in_int k (S l)) as (l',[],?). + auto. + replace l with l'. { trivial. } destruct (proj1 (Nat.lt_eq_cases l' l)); auto. * apply Nat.lt_succ_r; assumption. * absurd (exists_between k l). { auto. } apply in_int_exists with l'; auto. Qed.
imports: PeanoNat