length.v

  Lemma length_pair : forall {A : Type} (n : nat) (l : list A),
      length l <= n -> length (all_pairs l) <= n * n.
  Proof.
    intros A n l. generalize dependent n. induction l.
    intros n H. auto with arith.
    intros n H. destruct n.
    inversion H.
    simpl. simpl in H.
    repeat rewrite app_length. repeat rewrite map_length.
    Open Scope nat_scope.
    apply le_n_S. apply le_S_n in H.
    SearchAbout ( _ + _ <= _).
    
    
     
  A : Type
  a : A
  l : list A
  IHl : forall n : nat, length l <= n -> length (all_pairs l) <= n * n
  n : nat
  H : length l <= n
  ============================
  length (all_pairs l) + (length l + length l) <= n + n * S n