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 -> Q…