proposition: Theorem le_plus_minus' : forall n m:nat, m <= n -> n = m+(n-m).
proof: Proof. intros n m H; induction n. - rewrite (proj1 (Nat.le_0_r _) H); simpl; trivial. - Abort. End bad_proof_example_for_Induction1. Theorem lazy_example : forall n:nat, (S n) + 0 = S n. Proof. intros n; lazy beta iota zeta delta. fold plus. rewrite Nat.add_0_r; reflexivity. Qed.
imports: ZArith List Arith Lia