proposition: Lemma in_int_p_Sq : forall r p q a : nat, a >= 0 -> Between.in_int p (S q) r -> Between.in_int p q r \/ r = q \/ a = 0.
proof: Proof. hammer. Restart. hauto lq: on use: in_int_p_Sq. Qed.
imports: Hammer(Hammer) Arith List