3x < 5x

Coqでやってみた。

Require Import Arith. (* ring_simplify *)
Require Import Omega. (* omega *)

Theorem t1 (x:nat) : 3*(x+1) < 5*(x+1).
Proof.
  omega.
Qed.

Theorem t1' (x:nat) : 3*(x+1) < 5*(x+1).
Proof.
  induction x.
    simpl.
    auto.

    (* View -> Query Paneで(_<_)と打ってSearchする *)
    apply (plus_lt_compat_l (3*(x+1)) (5*(x+1)) 3) in IHx.
    apply (lt_plus_trans (3+3*(x+1)) (3+5*(x+1)) 2) in IHx.
    ring_simplify in IHx.
    ring_simplify.
    auto.
Qed.