All_pairs.v

Definition bounded_card (A: Type) (n: nat) :=  exists l, (forall a: A, In a l) /\ length l <= n.

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.
    
     Lemma length_cand : forall {A : Type} n , 
      bounded_card A n -> bounded_card (A * A) (n * n).
  Proof.
    intros A n. unfold Fixpoints.bounded_card.
    intros [l H]. exists (all_pairs l).
    destruct H as [H1 H2]. split. clear H2.
    intros (a1, a2). induction l.
    specialize (H1 a1). inversion H1.
    simpl.


 A : Type
  n : nat
  a : A
  l : list A
  H1 : forall a0 : A, In a0 (a :: l)
  a1, a2 : A
  IHl : (forall a : A, In a l) -> In (a1, a2) (all_pairs l)
  ============================
  (a, a) = (a1, a2) \/
  In (a1, a2) (all_pairs l ++ map (fun x : A => (a, x)) l ++ map (fun x : A => (x, a)) l)

subgoal 2 (ID 186) is:
 length (all_pairs l) <= n * n

A : Type
n : nat
a : A
l : list A
a1 : A
H1 : a = a1
a2 : A
IHl : (forall a : A, In a l) -> In (a1, a2) (all_pairs l)

(a, a) = (a1, a2)