length.v

 Lemma length_pair : forall {A : Type} (n : nat) (l : list A),
      length l <= n -> length (all_pairs l) <= n * n.
  Proof.
    intros. induction l.
    auto with arith.
    simpl. repeat rewrite app_length.
    repeat rewrite map_length.

  A : Type
  n : nat
  a : A
  l : list A
  H : length (a :: l) <= n
  IHl : length l <= n -> length (all_pairs l) <= n * n
  ============================
  S (length (all_pairs l) + (length l + length l)) <= n * n

Definition of all_pair

Fixpoint all_pairs {A: Type} (l: list A): list (A * A) :=
match l with
| [] => []
| c::cs => (c, c) :: (all_pairs cs)
++ (map (fun x => (c, x)) cs)
++ (map (fun x => (x, c)) cs)
end.