Section Test.

  Check 0.
  Check nat.
  Check Set.
  Check Type.
  Variable n : nat.
  Check n.
  Hypothesis n_is_positive : n > 0.
  Check n_is_positive.
  Check n > 0.
  Check Prop.
  Check gt.
  Check gt n.
  Check gt n 0.
End Test.

Section Example.
  Check S.
  Definition one := S 0.
  Check one.
  Definition double (m : nat) := plus m m.
  Check double one.
  Print double.
  Definition two := double one.
  Definition four := double two.
  Print four.
  Compute four.
  Definition gltf := forall m : nat, m < 4 \/ m >= 4.
  Check gltf.
  Print gltf.
End Example.

Section MinLog.
  Variables A B C : Prop.
  Check A -> B -> C.
  
  Goal A -> A.
  intro H.
  apply H.
  Save Identity.
  Print Identity.
  
  Lemma K : A -> B -> A.
  intros H1 H2.
  apply H1.
  Qed.

  Check K.

  Lemma S : (A -> B -> C) -> (A -> B) -> A -> C.
  intros.
  apply H; [ assumption | apply H0; assumption ].
  Qed.

  Lemma comconj : A /\ B -> B /\ A.
  intro.
  elim H.
  split; [ assumption | assumption ].
  Qed.

  Lemma deMorgan : (~A \/ ~B) -> ~(A /\ B).
  tauto.
  Qed.

  Print deMorgan.
End MinLog.

Section ClassLog.
  Hypothesis Stab : forall A : Prop, ~~A -> A.
  Variable A : Prop.
  Lemma lem : A \/ ~A.
    apply Stab.
    intro.
    apply H.
    apply or_intror.
    intro.
    apply H.
    apply or_introl.
    assumption.
  Qed.