Lemma ex_repeat : forall x, S (S (S x)) <= S (S (S (S (S (S (S x)))))).
intros x.
apply le_S.
(* bad solution,  try it : repeat (apply le_S || apply le_n).  *)
repeat (apply le_n || apply le_S).
Qed.

Lemma ex_repeat1 : 100 <= 200.
simpl.
Time repeat (apply le_n || apply le_S).
Qed.
Require Import List Arith Omega.

Ltac num_eq_list :=
  match goal with
    |- ?a::?b = ?c::?d =>
    let H := fresh in
    assert (H: a=c);[try ring; try omega | 
      try rewrite H; clear H; 
      assert (H : b = d);[apply refl_equal || num_eq_list | 
                          try rewrite H; apply refl_equal]]
  end.

Lemma ex_eq_list : forall a b c d, 
  a <= d -> d < a + 1 ->
  1+a::b+c::a+b::nil = a+1::c+b::b+d::nil.
intros.
num_eq_list.
Qed.

Require Arith.

Lemma minus_le : forall x y, x - y = 0 -> x <= y.
induction x; intros [ | y]; simpl; auto with arith; intros q; rewrite q; auto.
Qed.

Lemma ex_minus_le : 100 <= 200.
Time apply minus_le; simpl; auto.
Qed.

Hint Resolve le_n le_S : le_base.

Hint Rewrite plus_assoc : assoc_db.

Lemma ex_autorewrite : forall x y z t : nat,
  x + ((y+z)+t) = (x + y) + (z + t).
trivial.
intros.
Check plus_assoc.
 autorewrite with assoc_db; trivial.
Qed.