proposition: Lemma between_or_exists : forall k l, k <= l -> (forall n:nat, in_int k l n -> P n \/ Q n) -> between k l \/ exists_between k l.
proof: Proof. induction 1 as [|m ? IHle]. - auto. - intros P_or_Q. destruct IHle; auto. destruct (P_or_Q m); auto. Qed.
imports: PeanoNat