(** Omega **)


Require Import ZArith.

Lemma OM: forall f x y, 0 < x -> 0 < f x -> 3 * f x <= 2 * y -> f x <= y.
(* 
   A simple argument why it is true :
   f x <= 2/3 * y <= y (rationals)
   but f x and y are natural numbers, so
   f x <= y (nats)
*)
Proof. intros. omega.
Qed.

(* Caml Program for the proof *)
Print OM.

(* Changing y to y-1 in the conclusion *)
(*
   What's a simple argument for this?
   Hint : A similar argument as above.
*)
Lemma OM1 : forall f x y, 0 < x -> 0 < f x -> 3 * f x <= 2 * y -> f x <= y - 1.
Proof. intros. omega.
Qed.

(* Changing y to y-2 does not work. Try and see what happens *)





(** Logical Connectives **)


Lemma p20_1: forall A B C : Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
Proof. intros. destruct H as [H1 [H2 H3]].
split. split.
assumption. assumption. assumption.
Qed.

Print p20_1.

(* /\ is right associative in Coq *)
Lemma p20_11: forall A B C : Prop, A /\ B /\ C -> (A /\ B) /\ C.
Proof. intros.
(* if /\ is left associative, we would get H1 : A /\ B and H2 : C;
   if /\ is right associative, we would get H1 : A and H2 : B /\ C *)
destruct H as [H1 H2].
(* so, /\ is right associative! *)
(* rest of the proof is similar to p20_1. So, we will admit that
p20_11 is correct *)
Admitted.

Theorem p20_2 : forall A B C D : Prop, (A -> B) /\ (C -> D) /\ A /\ C -> B /\ D.
Proof. intros.  destruct H as [H1 [H2 [H3 H4]]]. split.
apply H1. assumption.
apply H2. assumption.
Qed.

Theorem p20_5 : forall A B : Prop, (A \/ B) /\ ~A -> B.
Proof. intros. destruct H as [[H1 | H2] H3].
case H3. assumption. assumption.
Qed.