proposition: Lemma in_int_lt2 : forall p q r : nat, Between.in_int p q r -> q >= p /\ r >= p /\ r <= q.
proof: Proof. hammer. Restart. sfirstorder use: Nat.lt_le_incl, in_int_lt unfold: ge, in_int. Qed.
imports: Hammer(Hammer) Arith List