proposition: Theorem comparison4 : 3 * q - 2 * p < q.
proof: Proof. apply Nat.add_lt_mono_l with (2 * p). rewrite Nat.add_comm; rewrite Nat.sub_add; try (simple apply Nat.lt_le_incl; auto with arith). replace (3 * q) with (2 * q + q); try ring. apply Nat.add_lt_le_mono; auto. repeat rewrite (Nat.mul_comm 2); apply mult_lt; auto with arith. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)