Section Minimal_Logic.

Variables A B C : Prop.

Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.

Lemma and_commutative : A /\ B -> B /\ A.

Lemma or_commutative : A \/ B -> B \/ A.

End Minimal_Logic.

Section Predicate_calculus.

Variable D : Set.

Variable R : D -> D -> Prop.

Section R_sym_trans.

Hypothesis R_symmetric : forall x y:D, R x y -> R y x.

Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.

Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.

End R_sym_trans.

Variable f : nat -> nat.

Hypothesis foo : f 0 = 0.

Lemma L1 : forall k:nat, k = 0 -> f k = k.

Hypothesis f10 : f 1 = f 0.

Lemma L2 : f (f 1) = 0.

Variable U : Type.

Definition set := U -> Prop.

Definition element (x:U) (S:set) := S x.

Definition subset (A B:set) := forall x:U, element x A -> element x B.

Definition transitive (T:Type) (R:T -> T -> Prop) :=
  forall x y z:T, R x y -> R y z -> R x z.

Lemma subset_transitive : transitive set subset.

End Predicate_calculus.

Section Inductive_types.

Inductive bool : Set := true | false.

Lemma duality : forall b:bool, b = true \/ b = false.

(*
  Inductive nat : Set :=
    | O : nat
    | S : nat -> nat.
*)

Fixpoint plus (n m:nat) {struct n} : nat :=
  match n with
    | O => m
    | S p => S (plus p m)
  end.

Lemma plus_n_O : forall n:nat, n = n + 0.

Definition Is_S (n:nat) := match n with
			     | O => False
			     | S p => True
			   end.

Lemma S_Is_S : forall n:nat, Is_S (S n).

Inductive le (n:nat) : nat -> Prop :=
  | le_n : le n n
  | le_S : forall m:nat, le n m -> le n (S m).

Lemma le_n_S : forall n m:nat, le n m -> le (S n) (S m).

Lemma tricky : forall n:nat, le n 0 -> n = 0.