Require Import SfLib.

Theorem diff_nsquared: 
   forall n,  (S n * S n) = (n*n) + n + n + 1.
Proof.
intros.
rewrite mult_succ_l.
rewrite mult_succ_r.
omega.
Qed.

Fixpoint f (n: nat) : nat :=
  match n with
  | O => O
  | S n => f n + 2*n + 1
  end.

Theorem f_square: forall n, f n = n * n.
Proof.
intros.
induction n as [|n'].
auto.
simpl.
rewrite IHn'.
rewrite mult_succ_r.
omega.
Qed.


Theorem ble_nat_e: forall n m, true = ble_nat n m -> n <= m.
Proof.
induction n as [|n']; intros.
omega.
destruct m; simpl in H.
inversion H.
apply IHn' in H.
omega.
Qed.

Theorem ble_nat_i: forall n m, n <= m -> true = ble_nat n m.
Proof.
induction n as [|n']; intros; simpl; auto.
destruct m.
elimtype False.
omega.
apply IHn'.
omega.
Qed.

Theorem false_ble_nat_i:  forall n m, n > m -> false = ble_nat n m.
Proof.
intros.
remember (ble_nat n m) as LE; destruct LE; auto.
apply ble_nat_e in HeqLE.
elimtype False.
omega.
Qed.

Theorem false_ble_nat_e: forall n m, false = ble_nat n m -> n > m.
Proof.
intros.
assert (n <= m \/ n > m) by omega.
destruct H0; auto.
apply ble_nat_i in H0.
rewrite <- H0 in H.
inversion H.
Qed.

Example example:  forall a b c d, 
    true = ble_nat a b -> 
    false = ble_nat c d -> 
    true = ble_nat (a+d) (b+c).
Proof.
intros.
(* Step one: Change hypotheses about ble_nat to hypotheses about le.  *)
 apply ble_nat_e in H. apply false_ble_nat_e in H0.
(* Step two: Change proof-goal about ble_nat to proof-goal about le. *)
apply ble_nat_i. 
(* Step three:  omega tactic can solve proof goals about lt, eq, gt,
  given hypotheses about lt, eq, gt of nats. *)
omega. 
Qed.