proposition: Lemma unprovable_le : forall n m:nat, n <= m.
proof: Proof. Time auto with arith. Time auto with le_base arith. Abort. Section bad_proof_for_auto. Section Trying_auto. Variable l1 : forall n m:nat, S n <= S m -> n <= m. Theorem unprovable_le2 : forall n m:nat, n <= m. Proof. Time auto with arith. Time try (clear l1; auto with arith; fail). Abort. End Trying_auto. End bad_proof_for_auto. Section combinatory_logic. Variables (CL:Set)(App:CL->CL->CL)(S:CL)(K:CL). Hypotheses (S_rule : forall A B C:CL, App (App (App S A) B) C = App (App A C)(App B C)) (K_rule : forall A B:CL, App (App K A) B = A). Hint Rewrite S_rule K_rule : CL_rules. Theorem obtain_I : forall A:CL, App (App (App S K) K) A = A. Proof. intros; autorewrite with CL_rules. reflexivity. Qed.
imports: ZArith List Arith Lia