exercise.v

Require Import Arith.

Module Exercise.
  (* Define a function that takes a natural number and returns it unchanged. *)
  Definition f := fun n : nat => n.

  (* Now prove the following simple fact about your function. *)
  Definition fact_1 := forall n, f n + 1 = f (n + 1).
  Lemma proof_1 : fact_1.
  Proof. unfold fact_1, f. reflexivity. Qed.

  (* Now prove another. *)
  Definition fact_2 := forall n, f n < f (n + 1).
  Lemma proof_2 : fact_2.
  Proof.
    unfold fact_2, f. intro n.
    rewrite Nat.add_1_r. apply le_n.
  Qed.
End Exercise.