Require Import Bool Arith Max Omega Psatz List NPeano Permutation.
Import List.ListNotations.

Require Import Unicode.Utf8_core.
Require Import Unicode.Utf8.
Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z) (at level 70, y at next level).
Notation "x < y ≤ z" := (x < y ∧ y ≤ z) (at level 70, y at next level).
Notation "x ≤ y < z" := (x ≤ y ∧ y < z) (at level 70, y at next level).

Infix "∈" := In (at level 70).

(* Compatibilité 8.4 *)
Infix "=?" := beq_nat (at level 70, no associativity).

Obligation Tactic := idtac.

Scheme Equality for prod.
Scheme Equality for list.

Set Implicit Arguments.

Section Trivial.
Lemma S_is_suc n: S n = n+1.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
Proof. omega. Qed.
Lemma or_idem: ∀ A, A ↔ A ∨ A.
Proof. tauto. Qed.
Lemma and_idem: ∀ A, A ↔ A ∧ A.
Proof. tauto. Qed.
Lemma and_left: ∀ A B, A ∧ B → A.
Proof. tauto. Qed.
Lemma or_false_idem: ∀ A, A ↔ A ∨ False.
Proof. tauto. Qed.

Definition fmono (f: nat → nat):= ∀ x y, x ≤ y → f x ≤ f y.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma forall_and {A:Type} (P Q:A→Prop):
  (∀ x, P x ∧ Q x) ↔ ((∀ x, P x) ∧ (∀ x, Q x)).
Proof. intuition; apply H. Qed.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma forall_impl_and {A:Type} (R:A→Prop) (P Q:A→Prop):
  (∀ x, R x → P x ∧ Q x) ↔
  ((∀ x, R x → P x) ∧ (∀ x, R x → Q x)).
Proof. intuition; now apply H. Qed.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma forall_impl2_and {A B:Type} (P Q R : A → B → Prop):
  (∀ x y, R x y → P x y ∧ Q x y) ↔ 
  ((∀ x y, R x y → P x y) ∧ (∀ x y, R x y → Q x y)).
Proof. intuition; now apply H. Qed.

Lemma eqb_subst_neq x y:
  x ≠ y → (x =? y) = false.
Proof. now rewrite Nat.eqb_neq. Qed.
Lemma neq_lt_gt_iff (m n:nat):
  m ≠ n ↔ (m < n ∨ n < m).
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
Proof. omega. Qed.

Lemma length_nil : forall A (l : list A),
  length l = 0 -> l = nil.
Proof.
(* Goal: forall (A : Type) (l : list A) (_ : @eq nat (@length A l) O), @eq (list A) l (@nil A) *)
 intros; destruct l; trivial; intros.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
 simpl in H; contradict H; omega.
Qed.
End Trivial.

Lemma prod_beq_eq A B
  (A_beq : A -> A -> bool) (B_beq : B -> B -> bool)
  (A_beq_eq : forall a1 a2, A_beq a1 a2 = true <-> a1 = a2) (B_beq_eq : forall b1 b2, B_beq b1 b2 = true <-> b1 = b2)
  p1 p2 : prod_beq _ _ A_beq B_beq p1 p2 = true <-> p1 = p2.
Proof.
(* Goal: iff (@NoDup A (@cons A a l)) (and (not (@In A a l)) (@NoDup A l)) *)
split; intro H.

- apply internal_prod_dec_bl with A_beq B_beq; trivial; firstorder.

- apply internal_prod_dec_lb; trivial; firstorder.
Qed.

Lemma list_beq_eq A
  (A_beq : A -> A -> bool) l1 l2 (A_beq_eq : forall a1 a2, In a1 l1 -> In a2 l2 -> (A_beq a1 a2 = true <-> a1 = a2)) :
  list_beq _ A_beq l1 l2 = true <-> l1 = l2.
Proof.
(* Goal: iff (@eq bool (list_beq A A_beq l1 l2) true) (@eq (list A) l1 l2) *)
revert l2 A_beq_eq.
(* Goal: forall (l2 : list A) (_ : forall (a1 a2 : A) (_ : @In A a1 l1) (_ : @In A a2 l2), iff (@eq bool (A_beq a1 a2) true) (@eq A a1 a2)), iff (@eq bool (list_beq A A_beq l1 l2) true) (@eq (list A) l1 l2) *)
induction l1 as [ | a1 l1 IH ]; intros [ | a2 l2 ] A_beq_eq; simpl; try tauto; try (split; congruence).
(* Goal: iff (@eq bool (andb (A_beq a1 a2) (list_beq A A_beq l1 l2)) true) (@eq (list A) (@cons A a1 l1) (@cons A a2 l2)) *)
simpl in A_beq_eq.
(* Goal: iff (@eq bool (andb (A_beq a1 a2) (list_beq A A_beq l1 l2)) true) (@eq (list A) (@cons A a1 l1) (@cons A a2 l2)) *)
rewrite andb_true_iff.
(* Goal: and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
split.

- intros [H1 H2].
(* Goal: @eq (list A) (@cons A a1 l1) (@cons A a2 l2) *)
  f_equal.

  + firstorder.

  + apply IH; auto.

- intros H.
(* Goal: and (@eq bool (A_beq a1 a2) true) (@eq bool (list_beq A A_beq l1 l2) true) *)
  injection H; clear H; intros; subst a2 l2.
(* Goal: and (@eq bool (A_beq a1 a1) true) (@eq bool (list_beq A A_beq l1 l1) true) *)
  split; [ apply A_beq_eq | apply IH ]; auto.
Qed.

Lemma list_beq_refl (A : Type) (A_beq : A -> A -> bool) l :
  (forall a1 a2 : A, In a1 l -> In a2 l -> (A_beq a1 a2 = true <-> a1 = a2)) ->
  list_beq _ A_beq l l = true.
Proof.
(* Goal: forall _ : forall (a1 a2 : A) (_ : @In A a1 l) (_ : @In A a2 l), iff (@eq bool (A_beq a1 a2) true) (@eq A a1 a2), @eq bool (list_beq A A_beq l l) true *)
intro A_beq_eq.
(* Goal: @eq bool (list_beq A A_beq l l) true *)
rewrite list_beq_eq; trivial.
Qed.

Lemma eq_None_neq_Some (A : Type) (x : option A) :
  x = None <-> forall v, x <> Some v.
Proof.
(* Goal: iff (@eq (option A) x (@None A)) (forall v : A, not (@eq (option A) x (@Some A v))) *)
destruct x; split; congruence.
Qed.

Lemma neq_None_eq_Some :
  forall (A: Type) (x: option A), x <> None <-> (exists a, x = Some a).
Proof.
(* Goal: iff (@NoDup A (@cons A a l)) (and (not (@In A a l)) (@NoDup A l)) *)
intros A [ a | ]; split; intro H.

- now exists a.

- congruence.

(* Goal: @NoDup A t1 *)
- tauto.

- destruct H as [ a H ].
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
  congruence.
Qed.

Lemma app_insert_r (A : Type) (l1 l1' l l2 l2' : list A):
  l1 ++ l2 = l1' ++ l2' -> length l2 = length l2' -> l1 ++ l ++ l2 = l1' ++ l ++ l2'.
Proof.
(* Goal: forall (_ : @eq (list A) (@app A l1 l2) (@app A l1' l2')) (_ : @eq nat (@length A l2) (@length A l2')), @eq (list A) (@app A l1 (@app A l l2)) (@app A l1' (@app A l l2')) *)
revert l1'.
(* Goal: forall (l1' : list A) (_ : @eq (list A) (@app A l1 l2) (@app A l1' l2')) (_ : @eq nat (@length A l2) (@length A l2')), @eq (list A) (@app A l1 (@app A l l2)) (@app A l1' (@app A l l2')) *)
induction l1 as [ | a1 l1 IH ]; simpl; intros l1' Heq Hlen.

- assert (l1' = []).
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
  {
(* Goal: le (S (@length A l)) (@length A l2) *)
    subst l2.
(* Goal: @eq (list A) l1' (@nil A) *)
    induction l1'; trivial.
(* Goal: @eq (list A) (@cons A a1 (@app A l1 (@app A l l2))) (@app A (@nil A) (@app A l (@cons A a1 (@app A l1 l2)))) *)
    rewrite app_length in Hlen.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
    simpl in Hlen; omega.
  }
(* Goal: @eq (list A) (@app A l l2) (@app A l1' (@app A l l2')) *)
  subst l1'.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
  simpl in *; congruence.

- destruct l1' as [ | a1' l1' ].

  + simpl in Heq.
(* Goal: @eq (list A) (@cons A a1 (@app A l1 (@app A l l2))) (@app A (@nil A) (@app A l l2')) *)
    subst l2'.
(* Goal: @eq (list A) (@cons A a1 (@app A l1 (@app A l l2))) (@app A (@nil A) (@app A l (@cons A a1 (@app A l1 l2)))) *)
    simpl in Hlen.
(* Goal: @eq (list A) (@cons A a1 (@app A l1 (@app A l l2))) (@app A (@nil A) (@app A l (@cons A a1 (@app A l1 l2)))) *)
    rewrite app_length in Hlen.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
    omega.

  + rewrite IH with (l1' := l1'); trivial; simpl in *; congruence.
Qed.

Section assoc.

Fixpoint assoc {A B : Type}(eq : A -> A -> bool)(x : A)(l : list (A * B)) : option B :=
  match l with
  | nil => None
  | (x', y) :: l' => if eq x x' then Some y else assoc eq x l'
  end.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Definition assoc_default {A B : Type}
  (eqA : A -> A -> bool) (d : B) (l : list (A * B)) (x : A) : B :=
  match assoc eqA x l with
  | None => d
  | Some b => b
  end.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma assoc_in {A B:Type} beq k (l: list (A * B)) {v}:
  (∀ a b:A, beq a b = true ↔ a=b) →
  assoc beq k l = Some v → (k,v) ∈ l.
Proof.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
intro.
(* Goal: forall _ : @eq (option B) (@assoc A B beq k l) (@Some B v), @In (prod A B) (@pair A B k v) l *)
induction l as [ | [a b] l1 IH ];try discriminate.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl. case_eq (beq k a);intros.
- left. rewrite H in H0. rewrite H0. congruence.
- right. apply IH;auto.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma assoc_None_not_in {A B:Type} beq k (l:list (A*B)):
  (∀ a b : A, beq a b = true ↔ a = b) →
  assoc beq k l = None ↔ ¬ k ∈ map fst l.
Proof.
(* Goal: @NoDup A t1 *)
intro Heq. induction l; simpl; try tauto.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
rewrite (surjective_pairing a). simpl.
(* Goal: iff (@eq (option B) (if beq k (@fst A B a) then @Some B (@snd A B a) else @assoc A B beq k l) (@None B)) (not (or (@eq A (@fst A B a) k) (@In A k (@map (prod A B) A (@fst A B) l)))) *)
case_eq (beq k (fst a)).
- rewrite Heq. intro. split; intros; try discriminate.
(* Goal: sumbool (lexprod (@pair A B a1 b1) (@pair A B a2 b2)) (not (lexprod (@pair A B a1 b1) (@pair A B a2 b2))) *)
  destruct H0. now left.
- intros. split; intros.
  + intro. destruct H1.
    * symmetry in H1. rewrite <- Heq in H1. rewrite H in H1. discriminate.
(* Goal: le (f m) n *)
    * rewrite IHl in H0. now destruct H0.
  + rewrite IHl. intro. destruct H0. now right.
Qed.

Lemma in_assoc_neq_None (A B: Type) (beq: A -> A -> bool) (k: A) (l: list (A * B)):
  (forall a b:A, a = b -> beq a b = true) ->
  In k (map (@fst _ _) l) ->
  assoc beq k l <> None.
Proof.
(* Goal: forall (_ : forall (a b : A) (_ : @eq A a b), @eq bool (beq a b) true) (_ : @In A k (@map (prod A B) A (@fst A B) l)), not (@eq (option B) (@assoc A B beq k l) (@None B)) *)
  intros Hbeq.
(* Goal: forall _ : @In A k (@map (prod A B) A (@fst A B) l), not (@eq (option B) (@assoc A B beq k l) (@None B)) *)
  revert k; induction l as [ | x l IH ]; intros k Hin.

  - exfalso; simpl in Hin; assumption.

  - simpl in Hin.
(* Goal: not (@eq (option B) (@assoc A B beq k (@cons (prod A B) x l)) (@None B)) *)
    destruct Hin as [ Heq | Hin ].

    + subst k.
(* Goal: not (@eq (option B) (@assoc A B beq (@fst A B x) (@cons (prod A B) x l)) (@None B)) *)
      destruct x as [ k v ].
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
      simpl.
(* Goal: not (@eq (option B) (if beq k k then @Some B v else @assoc A B beq k l) (@None B)) *)
      rewrite Hbeq; [ discriminate | exact eq_refl ].

    + destruct x as [ k' v' ].
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
      simpl.
(* Goal: not (@eq (option B) (if beq k k' then @Some B v' else @assoc A B beq k l) (@None B)) *)
      destruct (beq k k'); [ discriminate | idtac ].
(* Goal: not (@eq (option B) (@assoc A B beq k l) (@None B)) *)
      apply IH; assumption.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma assoc_in_Some {A B:Type} (beq:A→A→bool) (k:A) (l: list (A*B)):
  (∀ a b, beq a b = true ↔ a=b) →
  k ∈ map fst l ↔ ∃ v, v ∈ map snd l ∧ assoc beq k l = Some v.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
split; intros.
(* Goal: @NoDup A t1 *)
- induction l; simpl in *; try tauto. intuition.
  + exists (snd a). split; try left; auto.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    rewrite (surjective_pairing a), H1. simpl.
(* Goal: @eq (option B) (if beq k k then @Some B (@snd A B a) else @assoc A B beq k l) (@Some B (@snd A B a)) *)
    replace (beq k k) with true; auto. symmetry. now rewrite H.
  + case (beq k a0).
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    * exists b. simpl. auto.
(* Goal: le (f m) n *)
    * repeat destruct H0. exists x. auto.
- repeat destruct H0. rewrite in_map_iff. exists (k,x). split; auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
  apply (assoc_in beq); auto.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma assoc_in_Some_simple {A B:Type} beq k (l: list (A*B)):
  (∀ a b:A, beq a b = true ↔ a = b) →
  k ∈ map fst l ↔ (∃ v, assoc beq k l = Some v).
Proof.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
intro. split; intro.
- rewrite (assoc_in_Some beq) in H0; auto.
(* Goal: le (f m) n *)
  repeat destruct H0. eauto.
- destruct H0. generalize (assoc_in _ _ _ H H0).
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
  intro. rewrite in_map_iff. now exists (k, x).
Qed.


Lemma assoc_app_eq_None (A B:Type) (eq: A -> A -> bool) (x: A) (l1 l2: list (A * B)) :
  assoc eq x (l1 ++ l2) = None <-> (assoc eq x l1 = None /\ assoc eq x l2 = None).
Proof.
(* Goal: @NoDup A t1 *)
induction l1 as [ | [a b] l1 IH ]; try tauto.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: iff (@Logic.eq (option B) (if eq x a then @Some B b else @assoc A B eq x (@app (prod A B) l1 l2)) (@None B)) (and (@Logic.eq (option B) (if eq x a then @Some B b else @assoc A B eq x l1) (@None B)) (@Logic.eq (option B) (@assoc A B eq x l2) (@None B))) *)
case_eq (eq x a); trivial.
(* Goal: forall _ : @Logic.eq bool (eq x a) true, iff (@Logic.eq (option B) (@Some B b) (@None B)) (and (@Logic.eq (option B) (@Some B b) (@None B)) (@Logic.eq (option B) (@assoc A B eq x l2) (@None B))) *)
intro Hx.
(* Goal: iff (@Logic.eq (option B) (@Some B b) (@None B)) (and (@Logic.eq (option B) (@Some B b) (@None B)) (@Logic.eq (option B) (@assoc A B eq x l2) (@None B))) *)
split; [congruence | tauto].
Qed.

Lemma assoc_app_neq_None (A B:Type) (eq: A -> A -> bool) (x: A) (l1 l2: list (A * B)) :
  assoc eq x (l1 ++ l2) <> None <-> (assoc eq x l1 <> None \/ assoc eq x l2 <> None).
Proof.
(* Goal: @NoDup A t1 *)
induction l1 as [ | [a b] l1 IH ]; try tauto.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
case_eq (eq x a); auto with *.
Qed.

Lemma assoc_app_eq_Some (A B:Type) (eq: A -> A -> bool) (x: A) (v : B) (l1 l2: list (A * B)) :
  assoc eq x (l1 ++ l2) = Some v <->
  (assoc eq x l1 = Some v \/ (assoc eq x l1 = None /\ assoc eq x l2 = Some v)).
Proof.
(* Goal: and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
induction l1 as [ | [a b] l1 IH ]; simpl; split.

(* Goal: @NoDup A t1 *)
- tauto.

(* Goal: @NoDup A t1 *)
- intros [H1 | H1]; try congruence; tauto.

(* Goal: @NoDup A t1 *)
- case_eq (eq x a); tauto.

(* Goal: @NoDup A t1 *)
- case_eq (eq x a); try tauto.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
  intros H1 [ H2 | [ H2 H3 ] ]; congruence.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma assoc_app_in {K V:Type} beq k (l1 l2: list (K*V)):
  (∀ a b : K, beq a b = true ↔ a = b) →
  k ∈ map fst l1 → assoc beq k (l1++l2) = assoc beq k l1.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros. rewrite (assoc_in_Some_simple beq) in H0; auto.
(* Goal: @eq (option V) (@assoc K V beq k (@app (prod K V) l1 l2)) (@assoc K V beq k l1) *)
destruct H0. rewrite H0.
(* Goal: sumbool (lexprod (@pair A B a1 b1) (@pair A B a2 b2)) (not (lexprod (@pair A B a1 b1) (@pair A B a2 b2))) *)
rewrite assoc_app_eq_Some. now left.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma assoc_app_out {K V:Type} beq k (l1 l2: list (K*V)):
  (∀ a b : K, beq a b = true ↔ a = b) →
  ¬ k ∈ map fst l1 → assoc beq k (l1++l2) = assoc beq k l2.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
rewrite <- (assoc_None_not_in beq k l1 H) in H0.
case_eq (assoc beq k (l1 ++ l2)); intros.
- rewrite assoc_app_eq_Some in H1. destruct H1.
  + rewrite H0 in H1. discriminate.
  + now symmetry.
- rewrite assoc_app_eq_None in H1. now symmetry.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma assoc_in_concat {K V:Type} beq (k:K) ll (v:V):
  assoc beq k (concat ll) = Some v →
  ∃ l : list (K * V), l ∈ ll ∧ assoc beq k l = Some v.
(* not an iff. There might be l' before l with (k, v') in it *)
Proof.
(* Goal: and (@eq (list A) (@cons A a l1) (@nil A)) (@eq (list A) l2 l2') *)
induction ll; simpl; try discriminate.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
rewrite assoc_app_eq_Some. intuition; eauto.
(* Goal: le (f m) n *)
repeat destruct H0. eauto.
Qed.

End assoc.

Lemma map_in_ext :
  forall (A B : Type) (f g : A -> B) (l : list A),
  (forall a : A, In a l -> f a = g a) -> map f l = map g l.
Proof.
(* Goal: forall (A B : Type) (f g : forall _ : A, B) (l : list A) (_ : forall (a : A) (_ : @In A a l), @eq B (f a) (g a)), @eq (list B) (@map A B f l) (@map A B g l) *)
intros A B f g l H1; induction l as [ | a l IH ]; trivial.
(* Goal: @eq (list A) (@cons A a1 l1) (@cons A a2 l2) *)
simpl; f_equal.
(* Goal: @NoDup A t1 *)
apply H1; simpl; tauto.
(* Goal: @NoDup A t1 *)
apply IH; intros a' GH2; apply H1; simpl; tauto.
Qed.

Lemma incl_cons_cons A: forall (a:A) (l1 l2: list A), incl l1 l2 -> incl (a::l1) (a::l2).
Proof.
(* Goal: forall _ : forall (x : A) (_ : @In A x xs), @incl C (@flat_map B C rh (r x)) (lh x), @incl C (@flat_map B C rh (@concat B (@map A (list B) r xs))) (@flat_map A C lh xs) *)
unfold incl.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl. simpl in H0. destruct H0.
- left. auto.
- right. apply H. auto.
Qed.


Lemma map_incl A B (f : A -> B) l1 l2 : incl l1 l2 -> incl (map f l1) (map f l2).
Proof.
(* Goal: forall _ : @incl A l1 l2, @incl B (@map A B f l1) (@map A B f l2) *)
intros H x Hx.
(* Goal: @In B x (@map A B f l2) *)
apply in_map_iff in Hx.
(* Goal: @In B x (@map A B f l2) *)
apply in_map_iff.
(* Goal: @ex A (fun x0 : A => and (@eq B (f x0) x) (@In A x0 l2)) *)
destruct Hx as (y & Heq & Hy).
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
eauto.
Qed.

Lemma map_flat_map (A B C : Type) (f : A -> list B) (g : B -> C) (l : list A) :
map g (flat_map f l) = flat_map (fun a => map g (f a)) l.
Proof.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
induction l as [ | a l IH]; simpl.

- reflexivity.

- rewrite map_app, IH; reflexivity.
Qed.

Lemma incl_filter (A : Type) (f : A -> bool) l:
  incl (filter f l) l.
Proof.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
induction l as [ | x l IH ]; simpl; try congruence.
case (f x); auto with *.
Qed.

Lemma filter_ext_In {A : Type} f g (l : list A): (forall a , In a l -> f a = g a)-> filter f l = filter g l.
Proof.
(* Goal: forall _ : forall (a : A) (_ : @In A a l), @eq bool (f a) (g a), @eq (list A) (@filter A f l) (@filter A g l) *)
intro Heq.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- trivial.

- simpl. 
(* Goal: @eq (list A) (if f a then @cons A a (@filter A f l) else @filter A f l) (if g a then @cons A a (@filter A g l) else @filter A g l) *)
  rewrite Heq; [| left; trivial].
  case (g a); rewrite IHl; trivial; intro b; auto with *.
Qed.

Lemma filter_app A (f : A -> bool) l1 l2 : filter f (l1 ++ l2) = filter f l1 ++ filter f l2.
Proof.
(* Goal: @eq (list A) (@filter A f (@app A l1 l2)) (@app A (@filter A f l1) (@filter A f l2)) *)
induction l1.
- trivial.

- simpl.
  destruct (bool_dec (f a) true) as [Heq | Heq]; [ | apply not_true_is_false in Heq];
(* Goal: @NoDup A l *)
  rewrite Heq; rewrite IHl1; trivial.
Qed.

Lemma filter_flat_map A B f (g : A -> list B) l : filter f (flat_map g l) = flat_map (fun x => filter f (g x)) l.
Proof.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- trivial.

- simpl.
(* Goal: @eq (list B) (@filter B f (@app B (g a) (@flat_map A B g l))) (@app B (@filter B f (g a)) (@flat_map A B (fun x : A => @filter B f (g x)) l)) *)
  rewrite filter_app, IHl.
(* Goal: @NoDup A l *)
  trivial.
Qed.

Lemma flat_map_in_ext  A B (f g : A -> list B) l : 
  (forall a : A, In a l -> f a = g a) -> flat_map f l = flat_map g l.
Proof.
(* Goal: forall _ : forall (a : A) (_ : @In A a l), @eq bool (f a) (g a), @eq (list A) (@filter A f l) (@filter A g l) *)
induction l; intro Heq.
- trivial.

- simpl.
(* Goal: @eq (list B) (@app B (f a) (@flat_map A B f l)) (@app B (g a) (@flat_map A B g l)) *)
  rewrite Heq, IHl.
  + trivial.
  
  + intros.
(* Goal: @eq (list B) (f a0) (g a0) *)
    apply Heq.
(* Goal: @NoDup A l *)
    right; trivial.
    
  + left; trivial.
Qed.

Lemma NoDup_filter A f (l : list A) : NoDup l -> NoDup (filter f l).
Proof.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- trivial.

- intro H.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
  simpl.
  change (a:: l) with ([] ++ a :: l) in H.
(* Goal: @NoDup A (if f a then @cons A a (@filter A f l) else @filter A f l) *)
  assert (H2 := H).
(* Goal: @NoDup A (if f a then @cons A a (@filter A f l) else @filter A f l) *)
  apply NoDup_remove_1 in H; simpl in H.
(* Goal: @NoDup A (if f a then @cons A a (@filter A f l) else @filter A f l) *)
  apply NoDup_remove_2 in H2; simpl in H2.
  destruct (bool_dec (f a) true) as [Heq | Heq]; [ | apply not_true_is_false in Heq]; rewrite Heq;
(* Goal: @NoDup A t1 *)
  [apply NoDup_cons; [ rewrite filter_In |] |]; tauto.
Qed.

Lemma map_cons (A B : Type)(f : A -> B) a l : map f (a :: l) = f a :: map f l.
Proof.
(* Goal: @NoDup A l *)
trivial.
Qed.


Lemma length_remove A eq_A_dec (a: A) l :
  length (remove eq_A_dec a l) <= length l.
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a' l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
destruct (eq_A_dec a a') as [ Heq | Hneq ]; simpl; auto with *.
Qed.

Lemma length_cons_remove A eq_A_dec (a: A) l :
  In a l -> length (a :: remove eq_A_dec a l) <= length l.
Proof.
(* Goal: @NoDup A t1 *)
induction l as [ | a' l IH ]; simpl; try tauto.
(* Goal: forall _ : or (@eq A a' a) (@In A a l), le (S (@length A (if eq_A_dec a a' then @remove A eq_A_dec a l else @cons A a' (@remove A eq_A_dec a l)))) (S (@length A l)) *)
intros [ Heq | Hin ].

- subst a'.
(* Goal: @NoDup A t1 *)
  destruct (eq_A_dec a a) as [ _ | ]; try tauto.
(* Goal: le (Init.Nat.add (Init.Nat.add (g x) (S O)) (Init.Nat.add (suml (@map A nat g l)) (@length A l))) (Init.Nat.add (Init.Nat.add (g x) (suml (@map A nat g l))) (S (@length A l))) *)
  clear IH.
(* Goal: le (S (@length A l)) (S (@length A (@app A l3 l4))) *)
  apply le_n_S.
(* Goal: le (@length A (@remove A eq_A_dec a l)) (@length A l) *)
  apply length_remove.

- destruct (eq_A_dec a a') as [ Heq | Hneq ]; auto with *.
Qed.

Lemma neq_in_in_remove A eq_A_dec (a a': A) l:
  a' <> a -> In a l -> In a (remove eq_A_dec a' l).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a'' l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: forall (_ : not (@eq A a' a)) (_ : or (@eq A a'' a) (@In A a l)), @In A a (if eq_A_dec a' a'' then @remove A eq_A_dec a' l else @cons A a'' (@remove A eq_A_dec a' l)) *)
intros Hneq [ Heq | Hin ].

- subst a''.
(* Goal: @NoDup A t1 *)
  destruct (eq_A_dec a' a); simpl; tauto.

(* Goal: @NoDup A t1 *)
- destruct (eq_A_dec a' a''); simpl; tauto.
Qed.

Lemma incl_remove_app A l l1 l2 (x : A) : ~ In x l -> incl l (l1 ++ x :: l2) -> incl l (l1 ++ l2).
Proof.
(* Goal: forall (_ : not (@In A x l)) (_ : @incl A l (@app A l1 (@cons A x l2))), @incl A l (@app A l1 l2) *)
  intros Hnin Hincl.
(* Goal: @incl A l (@app A l1 l2) *)
    intros y Hyl.
    assert (Hyl2 : In y (l1 ++ x :: l2)) by apply Hincl, Hyl.
(* Goal: @In A y (@app A l1 l2) *)
    apply in_app_or in Hyl2.
(* Goal: @In A y (@app A l1 l2) *)
    destruct Hyl2 as [H1 | [Hx | H2]].
    + apply in_or_app.
(* Goal: or (@In A y l1) (@In A y l2) *)
      left; assumption.
    
    + elim Hnin.
(* Goal: @In A x l *)
      subst x.
(* Goal: not (@In A x l) *)
      assumption. 
    
    + apply in_or_app.
(* Goal: not (@In A x l) *)
      right; assumption.
Qed.



Lemma flat_map_nil (A B: Type) (f: A -> list B) (xs: list A):
  (forall x, In x xs -> f x = []) ->
  flat_map f xs = [].
Proof.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: @NoDup A l *)
induction xs as [ | x xs IH]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @NoDup A t1 *)
rewrite H, IH; trivial; auto with *; simpl; tauto.
Qed.

Lemma flat_map_comp (A B C : Type) (f : A -> B) (g : B -> list C) (h : A -> list C) (l : list A) :
  (forall x, In x l -> h x = g (f x)) -> flat_map h l = flat_map g (map f l).
Proof.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: @NoDup A l *)
induction l as [ | a l IH]; trivial.
simpl; rewrite IH, H; trivial; simpl; try tauto;
(* Goal: not (@In A x l) *)
intros; apply H; apply in_cons; assumption.
Qed.

Lemma flat_map_app (A B : Type) (f : A -> list B) l1 l2 :
  flat_map f (l1 ++ l2) = flat_map f l1 ++ flat_map f l2.
Proof.
(* Goal: @NoDup A l *)
induction l1 as [ | a1 l1 IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @eq (list B) (@app B (f a1) (@flat_map A B f (@app A l1 l2))) (@app B (@app B (f a1) (@flat_map A B f l1)) (@flat_map A B f l2)) *)
rewrite IH, app_assoc.
(* Goal: @NoDup A l *)
trivial.
Qed.

Lemma comp_flat_map (A B C : Type) (f : A -> list B) (g : B -> list C) h l :
  (forall a, In a l -> h a = flat_map g (f a)) -> flat_map h l = flat_map g (flat_map f l).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: le (Init.Nat.add (Init.Nat.add (g x) (S O)) (Init.Nat.add (suml (@map A nat g l)) (@length A l))) (Init.Nat.add (Init.Nat.add (g x) (suml (@map A nat g l))) (S (@length A l))) *)
rewrite IH; clear IH.

(* Goal: @NoDup A t1 *)
- rewrite H; try tauto.
(* Goal: forall _ : forall _ : @In nat n (@cons nat n l), and (le a n) (lt n (Init.Nat.add a O)), @eq nat (@length nat (@cons nat n l)) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec (@cons nat n l)) (seq a O))) *)
  clear H.
(* Goal: @NoDup A l *)
  rewrite flat_map_app; trivial.

(* Goal: @NoDup A t1 *)
- intros; apply H; tauto.
Qed.

Fixpoint andl (l : list Prop) : Prop :=
  match l with
  | nil => True
  | P :: l' => P /\ andl l'
  end.

Lemma andl_cons: forall a l, andl (a::l) <-> a /\ (andl l).
Proof.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
intros. simpl. intuition.
Qed.

Lemma andl_in : forall l P, andl l -> In P l -> P.
Proof.
(* Goal: forall (l : list Prop) (P : Prop) (_ : andl l) (_ : @In Prop P l), P *)
intros l P H1 H2; induction l as [ | P' l IH ]; simpl in H2.

(* Goal: @NoDup A t1 *)
- tauto.

(* Goal: @NoDup A t1 *)
- simpl in H1; destruct H2 as [ H2 | H2 ]; subst; tauto.
Qed.

Lemma andl_in_map (A:Type): forall l (a:A) P, andl (map P l) -> In a l -> P a.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
apply (andl_in (map P l));auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
apply in_map;auto.
Qed.

Lemma andl_map (A : Type) (f g : A -> Prop) l :
  andl (map f l) -> (forall a, In a l -> f a -> g a) -> andl (map g l).
Proof.
(* Goal: forall (_ : forall (a : A) (_ : @In A a l) (_ : P a), @ex B (fun b : B => Q a b)) (_ : @Forall A P l), @ex (list B) (fun l' : list B => @Forall2 A B Q l l') *)
intros H1 H2.
(* Goal: @NoDup A l *)
induction l as [ | a l IH]; trivial.
simpl in *.
(* Goal: and (g a) (andl (@map A Prop g l)) *)
destruct H1 as [H1 H3].
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
auto.
Qed.

Lemma andl_app l1 l2 : andl (l1 ++ l2) <-> andl l1 /\ andl l2.
Proof.
(* Goal: @NoDup A t1 *)
induction l1 as [ | P l1 IH ]; simpl; tauto.
Qed.

Fixpoint orl (l : list Prop) : Prop :=
  match l with
  | nil => False
  | P :: l' => P \/ orl l'
  end.

Lemma andl_concat l:
  andl (concat l) <-> forall l', In l' l -> andl l'.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
induction l; simpl; split; intros.
- now exfalso.
- auto.
- rewrite andl_app in H. destruct H. destruct H0.
  + subst l'. auto.
  + rewrite IHl in H1. apply H1. auto.
- rewrite andl_app. split.
  + apply H. auto.
  + rewrite IHl. intros. apply H. auto.
Qed.

Lemma orl_map (A : Type) (P : A -> Prop) l : orl (map P l) <-> exists x, In x l /\ P x.
Proof.
(* Goal: and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
split.

- induction l as [ | x l IH].

(* Goal: @NoDup A t1 *)
  + simpl; tauto.

  + simpl.
(* Goal: forall _ : or (@eq A a' a) (@In A a l), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @eq (list A) (@cons A a' l) (@app A l1 (@cons A a l2)))) *)
    intros [H | H].

    * exists x.
(* Goal: @NoDup A t1 *)
      tauto.

    * apply IH in H.
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 l)) (P x0)) *)
      destruct H as [x' H].
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 xs)) (R x0 y)) *)
      exists x'.
(* Goal: @NoDup A t1 *)
      tauto.

- intros [x [H1 H2] ].
(* Goal: @NoDup A l *)
  induction l as [ | y l IH]; trivial.
  simpl in *.
(* Goal: or (P y) (orl (@map A Prop P l)) *)
  destruct H1 as [H1 | H1].

  + subst y.
(* Goal: or (P x) (orl (@map A Prop P l)) *)
    left; exact H2.

  + right.
(* Goal: @NoDup A l1 *)
    apply IH.
(* Goal: @In A x l *)
    exact H1.
Qed.

Section Maxl.
Fixpoint maxl (l : list nat) : nat :=
  match l with
  | nil => 0
  | n :: l' => max n (maxl l')
  end.

Lemma maxl_is_max :
  forall l n, In n l -> n <= maxl l.
Proof.
intros l; induction l as [ | m l IH ]; intros n H; simpl in *.

(* Goal: @NoDup A t1 *)
- tauto.

- destruct H as [ H | H ].

  + subst m; apply le_max_l.

  + transitivity (maxl l).
(* Goal: @NoDup A l *)
    apply IH; trivial.
(* Goal: le (maxl (@map A nat g l)) (PeanoNat.Nat.max (g x) (maxl (@map A nat g l))) *)
    apply le_max_r.
Qed.

Lemma all_max_le l y :
  (forall x, In x l -> x <= y) -> maxl l <= y.
Proof.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
induction l as [ | x l IH]; simpl.

(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
- omega.

- destruct (max_dec x (maxl l)); firstorder.
Qed.

Lemma maxl_app : forall (l1 l2 : list nat), maxl (l1 ++ l2) = max (maxl l1) (maxl l2).
Proof.
(* Goal: @NoDup A l *)
intros l1 l2; induction l1 as [ | a1 l1 IH ]; trivial.
(* Goal: @eq nat (maxl (@app nat (@cons nat a1 l1) l2)) (PeanoNat.Nat.max (maxl (@cons nat a1 l1)) (maxl l2)) *)
simpl; rewrite IH; apply max_assoc.
Qed.

Lemma in_maxl (l : list nat) : l<>nil -> In (maxl l) l.
Proof.
(* Goal: forall _ : not (@eq (list nat) l (@nil nat)), @In nat (maxl l) l *)
induction l as [ | n l IH].

(* Goal: @NoDup A t1 *)
- tauto.

- intros _.
(* Goal: @In nat (maxl (@cons nat n l)) (@cons nat n l) *)
  destruct l as [ | m l].

  + simpl; left; symmetry; apply max_0_r.

  + change (maxl (n::m::l)) with (max n (maxl (m::l))).
(* Goal: @In nat (PeanoNat.Nat.max n (maxl (@cons nat m l))) (@cons nat n (@cons nat m l)) *)
    destruct (max_dec n (maxl (m::l))) as [H | H]; rewrite H.
(* Goal: @NoDup A t1 *)
    simpl; tauto.
(* Goal: and (@eq (list A) (@cons A a l1) (@nil A)) (@eq (list A) l2 l2') *)
    apply in_cons; apply IH; discriminate.
Qed.

Lemma all_maxl P xs: xs <> [] -> (forall x, In x xs -> P x) -> P (maxl xs).
Proof.
(* Goal: forall (_ : not (@eq (list nat) xs (@nil nat))) (_ : forall (x : nat) (_ : @In nat x xs), P x), P (maxl xs) *)
intros Hnotempty Hall.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
apply in_maxl in Hnotempty; auto.
Qed.

Lemma maxl_le_maxl A f g (l : list A) :
(forall x, In x l -> f x <= g x) -> maxl (map f l) <= maxl (map g l).
Proof.
(* Goal: forall (_ : @Forall A P xs) (_ : @In A x xs), P x *)
intro H1.
(* Goal: @NoDup A l *)
induction l as [ | x l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: le (PeanoNat.Nat.max (f x) (maxl (@map A nat f l))) (PeanoNat.Nat.max (g x) (maxl (@map A nat g l))) *)
destruct (max_dec (f x) (maxl (map f l))) as [ H2 | H2 ]; rewrite H2.

- transitivity (g x).

  + apply H1.
(* Goal: @NoDup A t1 *)
    simpl; tauto.

  + apply le_max_l.

- transitivity (maxl (map g l)).

  + apply IH.
(* Goal: forall (x : A) (_ : @In A x l), le (f x) (g x) *)
    intros x' H3.
(* Goal: le (maxl (@map A nat f l)) n *)
    apply H1.
(* Goal: @NoDup A t1 *)
    simpl; tauto.

  + apply le_max_r.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma maxl_map_const {A:Type} l (f: A → nat) n:
  (∀ x, x ∈ l → (f x) = n) →
  l ≠ [] → maxl (map f l) = n.
Proof.
(* Goal: @NoDup A t1 *)
induction l; simpl; intros; try tauto. clear H0.
destruct l; simpl in *.
- rewrite Nat.max_0_r. apply H. now left.
- replace (f a) with (n). replace (Nat.max (f a0) (maxl (map f l))) with (n).
  + apply Nat.max_id.
  + symmetry. apply IHl; try discriminate. intros. apply H. now right.
  + symmetry. apply H. now left.
Qed.

Lemma maxl_map_0 A l (f : A -> nat) : (* if n=0, we don't need l ≠ [] *)
  (forall x, In x l -> (f x) = 0) ->
  maxl (map f l) = 0.
Proof.
(* Goal: le (maxl l) (suml l) *)
destruct l.
- now simpl.
- intros. apply maxl_map_const; auto. discriminate.
Qed.

Lemma maxl_map_plus_le A f g (l : list A) :
  maxl (map (fun x => f x + g x) l) <= maxl (map f l) + maxl (map g l).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | x l IH]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
destruct (max_dec (f x + g x) (maxl (map (fun x0 : A => f x0 + g x0) l))) as [ H | H ];
(* Goal: forall _ : @eq nat (@length A la1) (@length B x), @Forall2 A B P la1 lb1 *)
rewrite H.

- apply plus_le_compat; apply le_max_l.

- etransitivity.

  + apply IH.

  + apply plus_le_compat; apply le_max_r.
Qed.

Lemma maxl_concat: forall l,
  maxl (concat l) = maxl (map maxl l).
Proof.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
induction l; simpl; auto.
(* Goal: @eq nat (if eq_dec a0 a then S (@count_occ A eq_dec (@app A l l') a) else @count_occ A eq_dec (@app A l l') a) (Init.Nat.add (if eq_dec a0 a then S (@count_occ A eq_dec l a) else @count_occ A eq_dec l a) (@count_occ A eq_dec l' a)) *)
rewrite maxl_app. rewrite IHl. reflexivity.
Qed.

Lemma maxl_map_lt_iff (A:Type): forall (l:list A) f n,
  0<n -> maxl (map f l) < n <-> (forall m, In m l -> (f m) < n).
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: iff (le (maxl (@map A nat f l)) n) (forall (m : A) (_ : @In A m l), le (f m) n) *)
induction l; simpl; split; intros; auto; try destruct IHl.
- now exfalso.
- destruct H1.
  + subst m.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply le_lt_trans with (m:=Nat.max (f a) (maxl (map f l))); auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply Nat.max_le_iff. auto.
  + apply H2; auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply le_lt_trans with (m:=Nat.max (f a) (maxl (map f l))); auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply Nat.max_le_iff. auto.
- apply Nat.max_lub_lt_iff. split.
  + apply H0. auto.
  + apply H2. intros. apply H0. auto.
Qed.

Lemma maxl_map_le_iff (A:Type): forall (l:list A) f n,
  maxl (map f l) <= n <-> (forall m, In m l -> (f m) <= n).
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: iff (le (maxl (@map A nat f l)) n) (forall (m : A) (_ : @In A m l), le (f m) n) *)
induction l; simpl; split; intros; auto; try destruct IHl.
- now exfalso.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
- omega.
- destruct H0.
  + subst m.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply le_trans with (m:=Nat.max (f a) (maxl (map f l))); auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply Nat.max_le_iff. auto.
  + apply H1; auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply le_trans with (m:=Nat.max (f a) (maxl (map f l))); auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    apply Nat.max_le_iff. auto.
- apply Nat.max_lub_iff. split.
  + apply H. auto.
  + apply H1. intros. apply H0; auto.
Qed.

Lemma maxl_map_is_max_map (A:Type): forall (l:list A) f a,
  In a l -> (f a) <= maxl (map f l).
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
induction l; simpl; intros.
- now exfalso.
- destruct H.
  + subst a. intuition.
  + apply Nat.max_le_iff. right.
(* Goal: le (f a0) (maxl (@map A nat f l)) *)
    now apply IHl.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma maxl_eq_maxl {A:Type} f g (l:list A):
  (∀ x : A, x ∈ l → f x = g x) →
  maxl (map f l) = maxl (map g l).
Proof. induction l; simpl; auto. Qed.
End Maxl.


Lemma in_concat_iff (A:Type) x (l:list (list A)):
  x ∈ concat l <-> exists l', l' ∈ l /\ x ∈ l'.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
induction l; simpl; split; intros.
(* Goal: @NoDup A t1 *)
- tauto.
(* Goal: @NoDup A t1 *)
- destruct H. tauto.
- rewrite in_app_iff in H. repeat destruct H.
  + exists a. auto.
(* Goal: @NoDup A t1 *)
  + rewrite IHl in H. destruct H. exists x0. tauto.
- rewrite in_app_iff. repeat destruct H.
  + left. auto.
  + right. rewrite IHl. exists x0. auto.
Qed.

Lemma incl_le_maxl :
  forall (l1 l2 : list nat), incl l1 l2 -> maxl l1 <= maxl l2.
Proof.
(* Goal: forall (l1 l2 : list nat) (_ : @incl nat l1 l2), le (maxl l1) (maxl l2) *)
intros l1 l2 H_incl.
(* Goal: le (maxl l1) (maxl l2) *)
case_eq l1.
- (* l1 = [] *)
(* Goal: forall _ : @eq (list nat) l1 (@nil nat), le (maxl (@nil nat)) (maxl l2) *)
  intro H_l1_empty.
(* Goal: le (maxl (@nil nat)) (maxl l2) *)
  unfold maxl.
(* Goal: le (@length A (@nil A)) (@length A l2) *)
  apply le_0_n.
- (* l1 = n :: l1' *)
  intros n l1' H_l1;
  subst l1; set (l1 := n :: l1').
(* Goal: le (maxl l1) (maxl l2) *)
  apply maxl_is_max.
(* Goal: @In nat (maxl l1) l2 *)
  apply H_incl.
(* Goal: @In nat (maxl (@cons nat n l)) (@cons nat n l) *)
  apply in_maxl.
(* Goal: and (@eq (list A) (@cons A a l1) (@nil A)) (@eq (list A) l2 l2') *)
  discriminate.
Qed.

Lemma maxl_cons : forall n l, maxl (n::l) = max n (maxl l).
Proof.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
auto.
Qed.

Lemma forall2_le_maxl :
  forall (l1 l2 : list nat), Forall2 le l1 l2 -> maxl l1 <= maxl l2.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: @NoDup A l *)
induction H;auto;simpl;apply Nat.max_le_compat;trivial.
Qed.

Lemma incl_flat_map (A B : Type) (f g : A -> list B) l :
  (forall a, In a l -> incl (f a) (g a)) ->
  incl (flat_map f l) (flat_map g l).
Proof.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
induction l as [ | a l IH ]; simpl; try congruence.
(* Goal: not (@eq A x y) *)
intro H.
apply incl_app; auto with *.
Qed.

Section suml.

Fixpoint suml (l : list nat) : nat :=
  match l with
  | nil => 0
  | n :: l' => n + suml l'
  end.

Lemma suml_cons n l : suml (n :: l) = n + suml l.
Proof.
(* Goal: @NoDup A l *)
trivial.
Qed.

Lemma suml_map_const A n (l : list A) : suml (map (fun _ => n) l) = n * length l.
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a l IH]; trivial.
(* Goal: @eq nat (suml (@map A nat (fun _ : A => n) (@cons A a l))) (Init.Nat.mul n (@length A (@cons A a l))) *)
simpl; lia.
Qed.

Lemma mult_suml_r m l : m * suml l = suml (map (fun n => m * n) l).
Proof.
(* Goal: @eq nat (Init.Nat.mul m (suml l)) (suml (@map nat nat (fun n : nat => Init.Nat.mul m n) l)) *)
induction l as [ | n l IH]; simpl; try ring.
(* Goal: @eq nat (Init.Nat.mul m (Init.Nat.add n (suml l))) (Init.Nat.add (Init.Nat.mul m n) (suml (@map nat nat (fun n : nat => Init.Nat.mul m n) l))) *)
rewrite mult_plus_distr_l.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
congruence.
Qed.

Lemma suml_app l1 l2 : suml (l1 ++ l2) = suml l1 + suml l2.
Proof.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
induction l1 as [ | n l1 IH]; simpl.

- reflexivity.

- rewrite IH; apply plus_assoc.
Qed.

Lemma suml_flat_map (A : Type)(f : A -> list nat)(l :list A) :
  suml (flat_map f l) = suml (map suml (map f l)).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | x l IH]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @eq nat (suml (@app nat (@map B nat g (f a)) (@flat_map A nat (fun x : A => @map B nat g (f x)) l))) (Init.Nat.add (suml (@map B nat g (f a))) (suml (@map A nat (fun x : A => suml (@map B nat g (f x))) l))) *)
rewrite suml_app.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
congruence.
Qed.

Lemma suml_flat_map_map (A B : Type) (f : A -> list B) (g : B -> nat) l :
  suml (flat_map (fun x => map g (f x)) l) = suml (map (fun x => suml (map g (f x))) l).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @eq nat (suml (@app nat (@map B nat g (f a)) (@flat_map A nat (fun x : A => @map B nat g (f x)) l))) (Init.Nat.add (suml (@map B nat g (f a))) (suml (@map A nat (fun x : A => suml (@map B nat g (f x))) l))) *)
rewrite suml_app.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
congruence.
Qed.

Lemma suml_map_plus (A : Type)(f g : A -> nat)(l : list A) : suml (map (fun x => f x + g x) l) = suml (map f l) + suml (map g l).
Proof.
(* Goal: @ex (list B) (fun l' : list B => @Forall2 A B Q l l') *)
induction l as [ | a l IH].

- trivial.

(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
- simpl; omega.
Qed.

Lemma suml_map_le :
  forall (A : Type)(f g : A -> nat)(l : list A),
  (forall x, In x l -> f x <= g x) -> suml (map f l) <= suml (map g l).
Proof.
(* Goal: forall (A : Type) (f g : forall _ : A, nat) (l : list A) (_ : forall (x : A) (_ : @In A x l), le (f x) (Init.Nat.add (g x) (S O))), le (suml (@map A nat f l)) (Init.Nat.add (suml (@map A nat g l)) (@length A l)) *)
intros A f g l H.
(* Goal: @NoDup A l *)
induction l as [ | x l IH ]; trivial.
(* Goal: le (suml (@map A nat f (@cons A x l))) (suml (@map A nat g (@cons A x l))) *)
simpl; apply plus_le_compat.

(* Goal: @NoDup A t1 *)
- apply H; simpl; tauto.

(* Goal: @NoDup A t1 *)
- apply IH; simpl in H; intros; apply H; tauto.
Qed.

Lemma suml_map_eq :
  forall (A : Type)(f g : A -> nat)(l : list A),
  (forall x, In x l -> f x = g x) -> suml (map f l) = suml (map g l).
Proof.
(* Goal: forall (A : Type) (f g : forall _ : A, nat) (l : list A) (_ : forall (x : A) (_ : @In A x l), le (f x) (Init.Nat.add (g x) (S O))), le (suml (@map A nat f l)) (Init.Nat.add (suml (@map A nat g l)) (@length A l)) *)
intros A f g l H.
(* Goal: @NoDup A l *)
induction l as [ | x l IH ]; trivial.
(* Goal: @eq nat (suml (@map A nat f (@cons A x l))) (suml (@map A nat g (@cons A x l))) *)
simpl; apply f_equal2.

(* Goal: @NoDup A t1 *)
- apply H; simpl; tauto.

(* Goal: @NoDup A t1 *)
- apply IH; simpl in H; intros; apply H; tauto.
Qed.


Lemma suml_map_le_plus_length :
  forall (A : Type)(f g : A -> nat)(l : list A),
  (forall x, In x l -> f x <= g x + 1) -> suml (map f l) <= suml (map g l) + length l.
Proof.
(* Goal: forall (A : Type) (f g : forall _ : A, nat) (l : list A) (_ : forall (x : A) (_ : @In A x l), le (f x) (Init.Nat.add (g x) (S O))), le (suml (@map A nat f l)) (Init.Nat.add (suml (@map A nat g l)) (@length A l)) *)
intros A f g l H.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
induction l as [ | x l IH ]; simpl; try omega.
transitivity (g x + 1 + (suml (map g l) + length l)).

- apply plus_le_compat; firstorder.

- clear IH.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
  omega.
Qed.

Lemma suml_le_len_times_bound l b :
  (forall x, In x l -> x <= b) -> suml l <= length l * b.
Proof.
(* Goal: forall _ : forall (x : nat) (_ : @In nat x l), le x b, le (suml l) (Init.Nat.mul (@length nat l) b) *)
induction l as [ | x' l' IH ].
- (* liste vide *)
(* Goal: @NoDup A l *)
  trivial.
- (* liste non vide *)
(* Goal: not (@eq A x y) *)
  intro H.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
  simpl.
(* Goal: le (Init.Nat.add x' (suml l')) (Init.Nat.add b (Init.Nat.mul (@length nat l') b)) *)
  apply plus_le_compat.
  + (* x' <= b *)
(* Goal: P (f x) *)
    apply H.
(* Goal: @NoDup A l *)
    trivial.
(* Goal: @In A x1 (@cons A x1 l1') *)
    apply in_eq.
  + (* suml l' <= length l' * b *)
(* Goal: @NoDup A l1 *)
    apply IH.
(* Goal: forall (x : nat) (_ : @In nat x l'), le x b *)
    intros x H_x_l'.
(* Goal: P (f x) *)
    apply H.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    simpl.
(* Goal: sumbool (@eq A x y) (not (@eq A x y)) *)
    right.
(* Goal: @NoDup A l *)
    trivial.
Qed.

Lemma in_le_suml :
  forall (n : nat)(l : list nat),
  In n l -> n <= suml l.
Proof.
(* Goal: forall (n : nat) (l : list nat) (_ : @In nat n l), le n (suml l) *)
induction l as [ | n' l IH ]; simpl; intro H_n_in.
- elim H_n_in.
- destruct H_n_in as [ H | H ].
  + subst n'.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
    omega.
  + apply IH in H.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
     omega.
Qed.

Lemma maxl_le_suml l: maxl l <= suml l.
Proof.
(* Goal: le (maxl l) (suml l) *)
destruct l.
- trivial.
- apply in_le_suml.
(* Goal: @In nat (maxl (@cons nat n l)) (@cons nat n l) *)
  apply in_maxl.
(* Goal: and (@eq (list A) (@cons A a l1) (@nil A)) (@eq (list A) l2 l2') *)
  discriminate.
Qed.

Lemma forall2_le_suml :
  forall (l1 l2 : list nat), Forall2 le l1 l2 -> suml l1 <= suml l2.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: @NoDup A l *)
induction H;auto;simpl;apply Plus.plus_le_compat;trivial.
Qed.

Lemma maxl_le_suml_map (A B : Type) (f : A -> list B) (g : B -> nat) (h : A -> nat) (l : list A) :
  (forall a, In a l -> maxl (map g (f a)) <= h a) ->
  maxl (map g (flat_map f l)) <= suml (map h l).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a l IH]; simpl; trivial.
intro H1; rewrite map_app, maxl_app;
destruct (max_dec (maxl (map g (f a))) (maxl (map g (flat_map f l)))) as [H2 | H2];
rewrite H2; clear H2.
(* Goal: @NoDup A t1 *)
- apply le_plus_trans; apply H1; tauto.
- etransitivity.
(* Goal: @NoDup A t1 *)
  + apply IH; intros; apply H1; tauto.
  + rewrite plus_comm; apply le_plus_trans; trivial.
Qed.

Lemma suml_map_mult_le_suml_mult_maxl (A : Type) f g (l : list A) :
  suml (map (fun x => f x * g x) l) <= suml (map f l) * maxl (map g l).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | x l IH]; trivial. 
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
etransitivity.
- apply plus_le_compat_l.
(* Goal: @NoDup A l1 *)
  apply IH.
- ring_simplify.
  apply plus_le_compat; apply mult_le_compat_l.
  + apply le_max_l.
  + apply le_max_r.
Qed.

Lemma suml_map_mult_le_suml_mult_suml (A : Type) f g (l : list A) :
  suml (map (fun x => f x * g x) l) <= suml (map f l) * suml (map g l).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | x l IH]; trivial. 
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
etransitivity.
- apply plus_le_compat_l.
(* Goal: @NoDup A l1 *)
  apply IH.
- ring_simplify.
  apply plus_le_compat_r.
  apply le_plus_trans.
  apply le_plus_l.
Qed.

Lemma length_flat_map (A B : Type) ( f : A -> list B) (l : list A) :
  length (flat_map f l) = suml (map (@length _) (map f l)).
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a l IH]; simpl; trivial.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
rewrite app_length; congruence.
Qed.

Lemma seq_Succ n m : seq n (S m) = seq n m ++ [m + n].
Proof.
(* Goal: @eq (list nat) (seq n (S m)) (@app nat (seq n m) (@cons nat (Init.Nat.add m n) (@nil nat))) *)
revert n.
(* Goal: forall n : nat, @eq (list nat) (seq n (S m)) (@app nat (seq n m) (@cons nat (Init.Nat.add m n) (@nil nat))) *)
induction m; intro n.
- trivial.
- simpl.
(* Goal: @eq (list nat) (@cons nat n (@cons nat (S n) (seq (S (S n)) m))) (@cons nat n (@app nat (seq (S n) m) (@cons nat (S (Init.Nat.add m n)) (@nil nat)))) *)
  rewrite plus_n_Sm.
  rewrite <- IHm.
(* Goal: @NoDup A l *)
  trivial.
Qed.

Lemma Permutation_filter {A : Type} f (l : list A) : Permutation l (filter f l ++ filter (fun x => negb (f x)) l).
Proof.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- simpl; trivial.
- simpl; case (f a).
  + simpl; auto.
  + simpl.
(* Goal: @NoDup A l *)
    apply Permutation_cons_app; trivial.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma filter_compose {A : Type} f g (l : list A) : 
  (forall x, In x l -> ( f x = true -> g x = true)) ->
  filter f (filter g l) = filter f l.
Proof.
(* Goal: not (@eq A x y) *)
induction l; intro H.
- trivial.
- simpl.
  assert (Ha : f a = true -> g a = true) by auto with *.
(* Goal: @eq (list A) (@filter A f (if g a then @cons A a (@filter A g l) else @filter A g l)) (if f a then @cons A a (@filter A f l) else @filter A f l) *)
  destruct (bool_dec (f a) true) as [HH | HH].
  + rewrite Ha; try trivial; simpl.
     rewrite HH, IHl; auto with *.
  + apply not_true_is_false in HH.
(* Goal: @eq (list A) (@filter A f (if g a then @cons A a (@filter A g l) else @filter A g l)) (if f a then @cons A a (@filter A f l) else @filter A f l) *)
    destruct (g a).
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    * simpl. rewrite IHl; auto with *.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    * simpl. rewrite HH, IHl; auto with *.
Qed.

(* dans 8.5 *)
Lemma in_seq : forall len start n : nat,
       In n (seq start len) <-> start <= n < start + len.
Proof.
(* Goal: forall len start n : nat, iff (@In nat n (seq start len)) (and (le start n) (lt n (Init.Nat.add start len))) *)
induction len; intros start n; split; intro H; simpl in H.
(* Goal: @NoDup A t1 *)
- tauto.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
- omega.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
- destruct H; [| apply IHlen in H]; omega.
- rewrite <- plus_n_Sm in H.
(* Goal: @In nat n (seq start (S len)) *)
  destruct H as [H1 H2].
(* Goal: and (@eq (list A) (@cons A a0 l1) (@cons A a0 l1')) (@eq (list A) l2 l2') *)
  destruct H1.
  + left; trivial.
  + right.
(* Goal: @In nat (S m) (seq (S start) len) *)
    apply lt_S_n in H2.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
    apply IHlen; omega.
Qed.

Lemma Permutation_partition_list_nat b n l :
 (forall x, In x l -> b <= x < b + n) ->
 Permutation l (flat_map (fun n => filter (beq_nat n) l) (seq b n)).
Proof.
revert b l; induction n; intros b l Hlt.
- simpl.
  destruct l as [ | h t].
  + trivial.
  + rewrite <- plus_n_O in Hlt.
    assert (Hf : b < b) by
      (apply le_lt_trans with h; apply Hlt; auto with *).
(* Goal: @NoDup A t1 *)
    apply lt_irrefl in Hf; tauto.
- simpl.
  etransitivity.
  + apply Permutation_filter with (f := beq_nat b).

  + apply Permutation_app.
    * trivial.
    * replace  (flat_map (fun n : nat => filter (beq_nat n) l) (seq (S b) n)) with 
            ((flat_map (fun n : nat => filter (beq_nat n) (filter (fun x : nat => negb (beq_nat b x)) l)) (seq (S b) n))).
       apply IHn.
(* Goal: forall (x : A) (_ : @In A x l), @Permutation B (f x) (g x) *)
       intros x Hx.
       apply filter_In in Hx.
       destruct Hx as [Hin Hneq].
       rewrite plus_Sn_m, plus_n_Sm.
       rewrite negb_true_iff in Hneq.
       apply beq_nat_false in Hneq.
       assert (b <= x) by (apply Hlt; tauto).
       assert (x < b + S n) by (apply Hlt; tauto).
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
       omega.

        apply flat_map_in_ext.
        intros a Ha.
        apply in_seq in Ha.
        simpl in Ha.
        apply filter_compose.
        intros x Hx Htrue.
        apply beq_nat_true in Htrue.
(* Goal: not (@In A x l') *)
        subst.
        apply negb_true_iff.
        apply Nat.eqb_neq.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
        omega.
Qed.

Lemma length_suml_filter b n l:
 (forall x, In x l -> b <= x < b + n) ->
 suml (map (fun r => length(filter (beq_nat r) l )) (seq b n)) = length l.
Proof.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: @eq nat (suml (@map nat nat (fun r : nat => @length nat (@filter nat (PeanoNat.Nat.eqb r) l)) (seq b n))) (@length nat l) *)
apply Permutation_partition_list_nat in H.
(* Goal: @eq nat (suml (@map nat nat (fun r : nat => @length nat (@filter nat (PeanoNat.Nat.eqb r) l)) (seq b n))) (@length nat l) *)
apply Permutation_length in H.
(* Goal: @eq nat (suml (@map nat nat (fun r : nat => @length nat (@filter nat (PeanoNat.Nat.eqb r) l)) (seq b n))) (@length nat l) *)
rewrite H, length_flat_map, map_map.
(* Goal: @NoDup A l *)
trivial.
Qed.

End suml.

Section prodl.

Fixpoint prodl (l : list nat) : nat :=
  match l with
  | nil => 1
  | n :: l' => n * prodl l'
  end.

Lemma prodl_bound (l : list nat) (b : nat) : 
  (forall x, In x l -> x <= b) -> prodl l <= Nat.pow b  (length l).
Proof.
(* Goal: forall _ : forall (x : nat) (_ : @In nat x l), le x b, le (prodl l) (Nat.pow b (@length nat l)) *)
induction l; intro Hb.
  - trivial.
  - simpl.
    apply mult_le_compat; auto with *.
Qed.

End prodl.


Definition clos_refl {A : Type} (R : A -> A -> Prop) (x y : A) : Prop :=
  R x y \/ x = y.

Lemma clos_refl_trans (A: Type) (R: A -> A -> Prop) t1 t2 t3:
    (R t1 t2 -> R t2 t3 -> R t1 t3) ->
    clos_refl R t1 t2 -> clos_refl R t2 t3 -> clos_refl R t1 t3.
Proof.
(* Goal: @clos_refl A R a a *)
unfold clos_refl.
(* Goal: @NoDup A t1 *)
intros H1 [H2 | H2] [H3 | H3]; subst; tauto.
Qed.

Lemma Forall2_eq_clos_refl (A:Type) (R: A -> A -> Prop) (l1 :list A) :
  Forall2 (clos_refl R) l1 l1.
Proof.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
induction l1;try auto.
(* Goal: @NoDup A l *)
apply Forall2_cons;trivial.
(* Goal: @clos_refl A R a a *)
unfold clos_refl.
(* Goal: @NoDup A l *)
right;trivial.
Qed.

Lemma Forall_In_l (A : Type) (P : A -> Prop) x xs:
  Forall P xs -> In x xs -> P x.
Proof.
(* Goal: forall (_ : @Forall A P xs) (_ : @In A x xs), P x *)
intro H1.
(* Goal: @NoDup A t1 *)
induction H1 as [ | x' xs H1 H2 H3]; simpl in *;try tauto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
intro H4;elim H4;clear H4;intro H4;auto.
(* Goal: not (@In A x l) *)
rewrite H4 in H1;assumption.
Qed.

Lemma Forall2_In_l (A B : Type) (R : A -> B -> Prop) x xs ys :
  Forall2 R xs ys -> In x xs -> exists y, In y ys /\ R x y.
Proof.
(* Goal: forall (_ : forall (a : A) (_ : @In A a l) (_ : P a), @ex B (fun b : B => Q a b)) (_ : @Forall A P l), @ex (list B) (fun l' : list B => @Forall2 A B Q l l') *)
intros H1 H2.
(* Goal: @NoDup A t1 *)
induction H1 as [ | x' y xs ys H1 H3 H4 ]; simpl in *; try tauto.
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 xs)) (R x0 y)) *)
destruct H2 as [ H2 | H2 ].
- subst x'.
(* Goal: @ex B (fun y0 : B => and (or (@eq B y y0) (@In B y0 ys)) (R x y0)) *)
  exists y.
(* Goal: @NoDup A t1 *)
  tauto.
- destruct (H4 H2) as (y' & H5 & H6).
(* Goal: @ex B (fun y0 : B => and (or (@eq B y y0) (@In B y0 ys)) (R x y0)) *)
  exists y'.
(* Goal: @NoDup A t1 *)
  tauto.
Qed.

Lemma Forall2_In_r (A B : Type) (R : A -> B -> Prop) y xs ys :
  Forall2 R xs ys -> In y ys -> exists x, In x xs /\ R x y.
Proof.
(* Goal: forall (_ : forall (a : A) (_ : @In A a l) (_ : P a), @ex B (fun b : B => Q a b)) (_ : @Forall A P l), @ex (list B) (fun l' : list B => @Forall2 A B Q l l') *)
intros H1 H2.
(* Goal: @NoDup A t1 *)
induction H1 as [ | x y' xs ys H1 H3 H4 ]; simpl in *; try tauto.
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 xs)) (R x0 y)) *)
destruct H2 as [ H2 | H2 ].
- subst y'.
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 xs)) (R x0 y)) *)
  exists x.
(* Goal: @NoDup A t1 *)
  tauto.
- destruct (H4 H2) as (x' & H5 & H6).
(* Goal: @ex A (fun x0 : A => and (or (@eq A x x0) (@In A x0 xs)) (R x0 y)) *)
  exists x'.
(* Goal: @NoDup A t1 *)
  tauto.
Qed.

Lemma Forall2_conj (A B : Type) (R1 R2 : A -> B -> Prop) xs ys :
  Forall2 R1 xs ys -> Forall2 R2 xs ys -> Forall2 (fun x y => R1 x y /\ R2 x y) xs ys.
Proof.
(* Goal: forall (_ : forall (a : A) (_ : @In A a l) (_ : P a), @ex B (fun b : B => Q a b)) (_ : @Forall A P l), @ex (list B) (fun l' : list B => @Forall2 A B Q l l') *)
intros H1 H2.
(* Goal: @NoDup A l *)
induction H1 as [ | x y xs ys H1 H3 H4 ]; trivial.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
inversion H2; auto.
Qed.

Lemma Forall2_trans (A: Type) (R: A -> A -> Prop) xs ys zs :
    (forall x y z, In x xs -> In y ys -> In z zs -> R x y -> R y z -> R x z) ->
    Forall2 R xs ys -> Forall2 R ys zs -> Forall2 R xs zs.
Proof.
(* Goal: forall (_ : forall (x y z : A) (_ : @In A x xs) (_ : @In A y ys) (_ : @In A z zs) (_ : R x y) (_ : R y z), R x z) (_ : @Forall2 A A R xs ys) (_ : @Forall2 A A R ys zs), @Forall2 A A R xs zs *)
intros H1 H2 H3.
(* Goal: @Forall2 A A R xs zs *)
revert xs H1 H2.
(* Goal: forall (xs : list A) (_ : forall (x y z : A) (_ : @In A x xs) (_ : @In A y ys) (_ : @In A z zs) (_ : R x y) (_ : R y z), R x z) (_ : @Forall2 A A R xs ys), @Forall2 A A R xs zs *)
induction H3 as [ | y z ys zs H3 H4 IH]; trivial; intros [ | x xs] H1 H2.
- inversion H2.
- inversion H2; subst.
(* Goal: @Acc (prod A B) lexprod (@pair A B a b) *)
  constructor.
  + apply H1 with y; try (simpl; tauto).
  + apply IH; trivial.
(* Goal: forall (x y z : A) (_ : @In A x xs) (_ : @In A y ys) (_ : @In A z zs) (_ : R x y) (_ : R y z), R x z *)
    intros x' y' z' H5 H7 H9 H10 H11.
(* Goal: @NoDup A t1 *)
    apply H1 with y'; simpl; tauto.
Qed.

Lemma Forall2_length A B (R : A -> B -> Prop) xs ys :
  Forall2 R xs ys -> length xs = length ys.
Proof.
(* Goal: forall _ : @Forall2 A B R xs ys, @eq nat (@length A xs) (@length B ys) *)
intros H.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
induction H; trivial; simpl; congruence.
Qed.

Lemma Forall2_map (A:Type) (B:Type): forall l f g (R:B->B->Prop),
  (forall (x:A), In x l -> R (f x) (g x)) -> Forall2 R (map f l) (map g l).
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- simpl;auto.
- simpl.
(* Goal: @Forall2 B B R (@cons B (f a) (@map A B f l)) (@cons B (g a) (@map A B g l)) *)
  apply Forall2_cons.
  + apply H;simpl;auto.    
  + apply IHl.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
    intros.
(* Goal: P (f x) *)
    apply H.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    simpl;right;auto.
Qed.

Lemma Forall2_flat_map (A B C D: Type) (R: C -> D -> Prop) (f: A -> list C) (g: B -> list D) (xs: list A) (ys: list B) :
  Forall2 (fun x y => Forall2 R (f x) (g y)) xs ys ->
  Forall2 R (flat_map f xs) (flat_map g ys).
Proof.
(* Goal: forall _ : @Exists2 A A R xs ys, @ex nat (fun i : nat => and (lt i (@length A xs)) (R (@nth A i xs d) (@nth A i ys d))) *)
revert ys.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
induction xs as [ | x xs IH]; intros [ | y ys] H1; simpl.
- constructor.
- inversion H1.
- inversion H1.
- inversion H1.
(* Goal: @NoDup A l *)
  apply Forall2_app; trivial.
(* Goal: @NoDup A l *)
  apply IH; trivial.
Qed.

Lemma Forall2_forall A (d: A) (R: A -> A -> Prop) (xs ys: list A) :
  Forall2 R xs ys ->
  forall i, i < length xs -> R (nth i xs d) (nth i ys d).
Proof.
(* Goal: forall _ : @Exists2 A A R xs ys, @ex nat (fun i : nat => and (lt i (@length A xs)) (R (@nth A i xs d) (@nth A i ys d))) *)
revert ys.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
induction xs as [ | x xs IH ]; simpl; intros ys H1 i H2; try omega.
(* Goal: @ex nat (fun i : nat => and (lt i (@length A (@cons A x xs))) (R (@nth A i (@cons A x xs) d) (@nth A i ys d))) *)
destruct ys as [ | y ys ]; try solve[inversion H1].
destruct i as [ | i ]; simpl; inversion H1; trivial; auto with *. 
Qed.

Inductive Exists2 {A B} (R: A -> B -> Prop) : list A -> list B -> Prop :=
 | Exists2_cons_hd : forall x xs y ys, R x y -> Exists2 R (x::xs) (y::ys)
 | Exists2_cons_tl : forall x xs y ys, Exists2 R xs ys -> Exists2 R (x::xs) (y::ys).
Hint Constructors Exists2.

Lemma Exists2_exists A (d: A) (R: A -> A -> Prop) (xs ys: list A) :
  Exists2 R xs ys ->
  exists i, i < length xs /\ R (nth i xs d) (nth i ys d).
Proof.
(* Goal: forall _ : @Exists2 A A R xs ys, @ex nat (fun i : nat => and (lt i (@length A xs)) (R (@nth A i xs d) (@nth A i ys d))) *)
revert ys.
(* Goal: forall (ys : list A) (_ : @Exists2 A A R xs ys), @ex nat (fun i : nat => and (lt i (@length A xs)) (R (@nth A i xs d) (@nth A i ys d))) *)
induction xs as [ | x xs IH ]; intros ys H1; try solve[inversion H1].
(* Goal: @ex nat (fun i : nat => and (lt i (@length A (@cons A x xs))) (R (@nth A i (@cons A x xs) d) (@nth A i ys d))) *)
destruct ys as [ | y ys ]; try solve[inversion H1].
(* Goal: not (@In A x l') *)
inversion H1 as [ aa ab ac ad Hxy af ag | aa ab ac ad Hxsys af ag ]; subst.
- exists 0.
(* Goal: @NoDup A l *)
  split; trivial.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
  simpl; omega.
- apply IH in Hxsys.
(* Goal: @ex nat (fun i : nat => and (lt i (@length A (@cons A x xs))) (R (@nth A i (@cons A x xs) d) (@nth A i (@cons A y ys) d))) *)
  destruct Hxsys as (i & Hi & HR ).
(* Goal: @ex nat (fun i : nat => and (lt i (@length A (@cons A x xs))) (R (@nth A i (@cons A x xs) d) (@nth A i (@cons A y ys) d))) *)
  exists (S i).
(* Goal: @NoDup A l *)
  split; trivial.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
  simpl; omega.
Qed.

Lemma app_eq_compat_l {A: Type} (xs ys zs: list A) : ys = zs -> xs ++ ys = xs ++ zs.
Proof.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
induction xs as [ | x xs IH ]; trivial; congruence.
Qed.

Lemma In_prefix_suffix (A : Type) (a : A) l :
  In a l -> exists l1 l2, l = l1 ++ a :: l2.
Proof.
(* Goal: @NoDup A t1 *)
induction l as [ | a' l IH ]; simpl; try tauto.
(* Goal: forall _ : or (@eq A a' a) (@In A a l), @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @eq (list A) (@cons A a' l) (@app A l1 (@cons A a l2)))) *)
intros [ H | H ].
- subst a'.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A y l) (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A y l) (@app A l1 (@cons A y (@app A l2 (@cons A x l3)))))))) *)
  exists [].
(* Goal: @ex (list A) (fun l2 : list A => @eq (list A) (@cons A a l) (@app A (@nil A) (@cons A a l2))) *)
  exists l.
(* Goal: @NoDup A l *)
  trivial.
- apply IH in H.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @eq (list A) (@cons A a' l) (@app A l1 (@cons A a l2)))) *)
  destruct H as (l1 & l2 & H).
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @eq (list A) (@cons A a' l) (@app A l1 (@cons A a l2)))) *)
  subst l.
(* Goal: @ex (list A) (fun l3 : list A => @ex (list A) (fun l4 : list A => @eq (list A) (@cons A a' (@app A l1 (@cons A a l2))) (@app A l3 (@cons A a l4)))) *)
  exists (a' :: l1).
(* Goal: @ex (list A) (fun l3 : list A => @eq (list A) (@cons A a' (@app A l1 (@cons A a l2))) (@app A (@cons A a' l1) (@cons A a l3))) *)
  exists l2.
(* Goal: @NoDup A l *)
  trivial.
Qed.

Lemma forall_exists_list (A B : Type) (P : A -> Prop) (Q : A -> B -> Prop) (l : list A) :
  (forall a, In a l -> P a -> exists b, Q a b) ->
  (Forall P l -> exists l', Forall2 Q l l').
Proof.
(* Goal: forall (_ : forall (a : A) (_ : @In A a l) (_ : P a), @ex B (fun b : B => Q a b)) (_ : @Forall A P l), @ex (list B) (fun l' : list B => @Forall2 A B Q l l') *)
intros H1 H2.
(* Goal: @ex (list B) (fun l' : list B => @Forall2 A B Q l l') *)
induction l as [ |a l IH ].
- exists [].
(* Goal: @NoDup A l *)
  trivial.
(* Goal: @NoDup A t1 *)
- destruct (H1 a) as [ b Hb ]; simpl; try tauto.
  + inversion H2; trivial.
  + destruct IH as [l' Hl']; auto with *.
    * inversion H2; trivial.
    * exists (b :: l').
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
      auto.
Qed.

Lemma forall_andl (A: Type) (P: A -> Prop) (l: list A):
  Forall P l <-> andl (map P l).
Proof.
(* Goal: and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
split.
- induction l as [ | x l' ].
  + intros; simpl; trivial.
  + intros Hfor.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    simpl.
(* Goal: and (P x) (andl (@map A Prop P l')) *)
    inversion Hfor.
(* Goal: and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
    split.
    * assumption.
    * apply IHl'; assumption.
- induction l as [ | x l' ].
  + intros; simpl; trivial.
  + simpl.
(* Goal: forall _ : and (P x) (andl (@map A Prop P l')), @Forall A P (@cons A x l') *)
    intros ( HPx & Handl' ).
(* Goal: @Acc (prod A B) lexprod (@pair A B a b) *)
    constructor.
    * assumption.
    * apply IHl'; assumption.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Fixpoint revflatten {A: Type} (xss: list (list A)) : list A :=
  match xss with
  | []       => []
  | xs::xss' => revflatten xss' ++ xs
  end.

Lemma Permutation_flat_map_ext A B  : forall l (f g : A -> list B),
  (forall x, In x l -> Permutation (f x) (g x)) -> Permutation (flat_map f l) (flat_map g l).
Proof.
(* Goal: forall (l : list A) (f g : forall _ : A, list B) (_ : forall (x : A) (_ : @In A x l), @Permutation B (f x) (g x)), @Permutation B (@flat_map A B f l) (@flat_map A B g l) *)
 induction l; intros f g H.
  - apply Permutation_refl.
  - simpl.
(* Goal: @Permutation B (@app B (f a) (@flat_map A B f l)) (@app B (g a) (@flat_map A B g l)) *)
    apply Permutation_app.
    +  apply H. apply in_eq.
    + apply IHl.
(* Goal: forall (x : A) (_ : @In A x l), @Permutation B (f x) (g x) *)
      intros x Hx.
(* Goal: not (@In A x l) *)
      apply H; apply in_cons; assumption.
Qed.

Lemma Permutation_revflatten A B (f : A -> list B) l : Permutation(revflatten (map f l)) (flat_map f l).
Proof.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- apply Permutation_refl.
- simpl.
  eapply Permutation_trans.
  + apply Permutation_app_comm.

  + apply Permutation_app; [apply Permutation_refl | assumption].
Qed.

Lemma In_seq n start len : In n (seq start len) <-> start <= n < start+len.
Proof.
(* Goal: @eq (list nat) (@cons nat start (seq (S start) len)) (@app nat (seq start len) (@cons nat (Init.Nat.add start len) (@nil nat))) *)
revert start.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
induction len as [ | len IH ]; intro start; simpl; try omega.
(* Goal: iff (or (@eq nat start n) (@In nat n (seq (S start) len))) (and (le start n) (lt n (Init.Nat.add start (S len)))) *)
rewrite IH.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
omega.
Qed.

Lemma seq_S start len : seq start (S len) = seq start len ++ [start + len].
Proof.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @eq (list nat) (@cons nat start (seq (S start) len)) (@app nat (seq start len) (@cons nat (Init.Nat.add start len) (@nil nat))) *)
revert start.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
induction len as [ | len IH ]; intro start; simpl.
- rewrite plus_0_r.
(* Goal: @NoDup A l *)
  trivial.
- rewrite IH, plus_Snm_nSm.
(* Goal: @NoDup A l *)
  trivial.
Qed.

Lemma plus_eq_compat_l x y1 y2 : y1 = y2 -> x + y1 = x + y2.
Proof.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
congruence.
Qed.

Lemma plus_eq_compat_r x1 x2 y : x1 = x2 -> x1 + y = x2 + y.
Proof.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
congruence.
Qed.


Section count_occ.

Lemma count_occ_remove_O A eq_dec (a: A) l :
  count_occ eq_dec (remove eq_dec a l) a = 0.
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a' l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @NoDup A l *)
destruct (eq_dec a a') as [ | Hneq]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
destruct (eq_dec a' a); trivial; congruence.
Qed.

Lemma count_occ_remove_neq A eq_dec (a a': A) l :
  a<>a' -> count_occ eq_dec (remove eq_dec a' l) a = count_occ eq_dec l a.
Proof.
(* Goal: forall _ : not (@eq A a a'), @eq nat (@count_occ A eq_dec (@remove A eq_dec a' l) a) (@count_occ A eq_dec l a) *)
intro Hneq.
(* Goal: @NoDup A l *)
induction l as [ | a'' l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @eq nat (@count_occ A eq_dec (if eq_dec a' a'' then @remove A eq_dec a' l else @cons A a'' (@remove A eq_dec a' l)) a) (if eq_dec a'' a then S (@count_occ A eq_dec l a) else @count_occ A eq_dec l a) *)
destruct (eq_dec a' a'') as [ Heq | Hneq'].
- subst a''.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
  destruct (eq_dec a' a); trivial; congruence.
- simpl.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
destruct (eq_dec a'' a); trivial; congruence.
Qed.

Lemma suml_map_count_occ_remove A eq_dec (a: A) l1 l2 :
  ~In a l2 ->
  suml (map (count_occ eq_dec (remove eq_dec a l1)) l2) =
  suml (map (count_occ eq_dec l1) l2).
Proof.
(* Goal: forall _ : not (@In A a l2), @eq nat (suml (@map A nat (@count_occ A eq_dec (@remove A eq_dec a l1)) l2)) (suml (@map A nat (@count_occ A eq_dec l1) l2)) *)
revert a l1.
(* Goal: @NoDup A l *)
induction l2 as [ | a' l2 IH ]; intros a l1 Hnotin; trivial.
simpl in *.
(* Goal: @NoDup A t1 *)
assert (a' <> a /\ ~In a l2) as [Hneq Hnotin'] by tauto.
(* Goal: @eq nat (Init.Nat.add (@count_occ A eq_dec (@remove A eq_dec a l1) a') (suml (@map A nat (@count_occ A eq_dec (@remove A eq_dec a l1)) l2))) (Init.Nat.add (@count_occ A eq_dec l1 a') (suml (@map A nat (@count_occ A eq_dec l1) l2))) *)
apply IH with (l1 := l1) in Hnotin'.
(* Goal: @eq nat (Init.Nat.add (@count_occ A eq_dec (@remove A eq_dec a l1) a') (suml (@map A nat (@count_occ A eq_dec (@remove A eq_dec a l1)) l2))) (Init.Nat.add (@count_occ A eq_dec l1 a') (suml (@map A nat (@count_occ A eq_dec l1) l2))) *)
rewrite Hnotin'.
(* Goal: @eq nat (Init.Nat.add (@count_occ A eq_dec (@remove A eq_dec a l1) a') (suml (@map A nat (@count_occ A eq_dec l1) l2))) (Init.Nat.add (@count_occ A eq_dec l1 a') (suml (@map A nat (@count_occ A eq_dec l1) l2))) *)
apply plus_eq_compat_r.
(* Goal: @NoDup A l *)
apply count_occ_remove_neq; trivial.
Qed.

Lemma length_remove_count_occ A eq_dec (a: A) l:
  length l = length (remove eq_dec a l) + count_occ eq_dec l a.
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a' l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @eq nat (S (@length A l)) (Init.Nat.add (@length A (if eq_dec a a' then @remove A eq_dec a l else @cons A a' (@remove A eq_dec a l))) (if eq_dec a' a then S (@count_occ A eq_dec l a) else @count_occ A eq_dec l a)) *)
destruct (eq_dec a a') as [ Heq | Hneq ].
- subst a'.
(* Goal: @eq nat (S (@length A l)) (Init.Nat.add (@length A (@remove A eq_dec a l)) (if eq_dec a a then S (@count_occ A eq_dec l a) else @count_occ A eq_dec l a)) *)
  destruct (eq_dec a a); [ omega | tauto ].
- simpl.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
  destruct (eq_dec a' a); congruence.
Qed.

Lemma in_remove_neq A eq_dec (a a': A) l :
  In a' (remove eq_dec a l) -> In a' l.
Proof.
(* Goal: @NoDup A l *)
induction l as [ | a'' l IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @NoDup A t1 *)
destruct (eq_dec a a''); simpl; tauto.
Qed.

Lemma length_count_occ a b l :
  (forall n, In n l -> a <= n < a + b) ->
  length l = suml (map (count_occ eq_nat_dec l) (seq a b)).
Proof.
(* Goal: forall _ : forall (n : nat) (_ : @In nat n l), and (le a n) (lt n (Init.Nat.add a b)), @eq nat (@length nat l) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec l) (seq a b))) *)
revert a l.
(* Goal: forall (a : nat) (l : list nat) (_ : forall (n : nat) (_ : @In nat n l), and (le a n) (lt n (Init.Nat.add a b))), @eq nat (@length nat l) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec l) (seq a b))) *)
induction b as [ | b IH ]; intros a l.
- intro H.
(* Goal: @NoDup A l *)
  destruct l as [ | n l ]; trivial.
(* Goal: @eq nat (@length nat (@cons nat n l)) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec (@cons nat n l)) (seq a O))) *)
  generalize (H n).
(* Goal: forall _ : forall _ : @In nat n (@cons nat n l), and (le a n) (lt n (Init.Nat.add a O)), @eq nat (@length nat (@cons nat n l)) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec (@cons nat n l)) (seq a O))) *)
  clear H.
(* Goal: not (@eq A x y) *)
  intro H.
(* Goal: @eq nat (@length nat (@cons nat n l)) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec (@cons nat n l)) (seq a O))) *)
  assert (H1: In n (n::l)) by (simpl; tauto).
(* Goal: @eq nat (@length nat (@cons nat n l)) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec (@cons nat n l)) (seq a O))) *)
  apply H in H1.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
  omega.
- intro H.
  replace (seq a (S b)) with (seq a b ++ [a + b])
   by (symmetry; apply seq_S).
(* Goal: @eq nat (@length nat l) (suml (@map nat nat (@count_occ nat PeanoNat.Nat.eq_dec l) (@app nat (seq a b) (@cons nat (Init.Nat.add a b) (@nil nat))))) *)
  rewrite map_app, suml_app.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
  simpl.
  replace (suml (map (count_occ eq_nat_dec l) (seq a b)))
   with (suml (map (count_occ eq_nat_dec (remove eq_nat_dec (a+b) l)) (seq a b))).
  + rewrite <- IH.
    * rewrite plus_0_r.
(* Goal: @eq nat (@length nat l) (Init.Nat.add (@length nat (@remove nat PeanoNat.Nat.eq_dec (Init.Nat.add a b) l)) (@count_occ nat PeanoNat.Nat.eq_dec l (Init.Nat.add a b))) *)
      apply length_remove_count_occ.
    * intros n Hn.
      { destruct (eq_nat_dec n (a+b)) as [ Heq | Hneq ].
      - subst n.
        generalize (remove_In eq_nat_dec l (a+b)).
(* Goal: @NoDup A t1 *)
        tauto.
      - assert (Hin: In n l).
        + apply in_remove_neq in Hn; trivial.
        + apply H in Hin.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
          omega.
      }
  + apply suml_map_count_occ_remove.
(* Goal: not (@In nat (Init.Nat.add a b) (seq a b)) *)
    clear.
(* Goal: not (@In nat (Init.Nat.add a b) (seq a b)) *)
    rewrite In_seq.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
    omega.
Qed.

Lemma count_occ_cons A eq_dec (a a': A) l :
  count_occ eq_dec (a::l) a' =
  if eq_dec a a' then S (count_occ eq_dec l a') else count_occ eq_dec l a'.
Proof.
(* Goal: @NoDup A l *)
trivial.
Qed.

Lemma count_occ_app A eq_dec (a :A) l l' :
  count_occ eq_dec (l ++ l') a = count_occ eq_dec l a + count_occ eq_dec l' a.
Proof.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
  induction l.
  - trivial.
  - simpl app.
(* Goal: @eq nat (if eq_dec a0 a then S (@count_occ A eq_dec (@app A l l') a) else @count_occ A eq_dec (@app A l l') a) (Init.Nat.add (@count_occ A eq_dec (@cons A a0 l) a) (@count_occ A eq_dec l' a)) *)
    rewrite count_occ_cons.
(* Goal: @eq nat (if eq_dec a0 a then S (@count_occ A eq_dec (@app A l l') a) else @count_occ A eq_dec (@app A l l') a) (Init.Nat.add (@count_occ A eq_dec (@cons A a0 l) a) (@count_occ A eq_dec l' a)) *)
    rewrite count_occ_cons.
(* Goal: @eq nat (if eq_dec a0 a then S (@count_occ A eq_dec (@app A l l') a) else @count_occ A eq_dec (@app A l l') a) (Init.Nat.add (if eq_dec a0 a then S (@count_occ A eq_dec l a) else @count_occ A eq_dec l a) (@count_occ A eq_dec l' a)) *)
    rewrite IHl.
(* Goal: @NoDup A l *)
    case (eq_dec a0 a); trivial.
Qed.

Lemma count_occ_flat_map A B eq_B_dec (f: A -> list B) b l :
  count_occ eq_B_dec (flat_map f l) b =
  suml (map (fun a => count_occ eq_B_dec (f a) b) l).
Proof.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
  induction l.
  - trivial.
  - simpl.
(* Goal: @eq nat (@count_occ B eq_B_dec (@app B (f a) (@flat_map A B f l)) b) (Init.Nat.add (@count_occ B eq_B_dec (f a) b) (suml (@map A nat (fun a : A => @count_occ B eq_B_dec (f a) b) l))) *)
    rewrite count_occ_app.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
    auto.
Qed.

End count_occ.

Lemma tl_incl (A:Type): forall (a:A) l l', incl (a::l') l -> incl l' l.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
apply incl_tran with (m:=a::l');auto.
(* Goal: @incl A l' (@cons A a l') *)
apply incl_tl;apply incl_refl.
Qed.

Section NoDup.

Lemma NoDup_app (A: Type) (l1 l2: list A):
  (forall x, In x l1 -> ~ In x l2) ->
  NoDup l1 ->
  NoDup l2 ->
  NoDup (l1 ++ l2).
Proof.
(* Goal: forall _ : @incl A l1 l2, le (@length A l1) (@length A l2) *)
  revert l2.
  induction l1 as [ | x1 l1' IH ];
    intros l2 Hnotin Hnodup1 Hnodup2.
  - rewrite app_nil_l.
(* Goal: @NoDup A l2 *)
    exact Hnodup2.
  - rewrite <- app_comm_cons.
(* Goal: @Acc (prod A B) lexprod (@pair A B a b) *)
    constructor.
    + rewrite in_app_iff.
(* Goal: not (or (@In A x1 l1') (@In A x1 l2)) *)
      intros Hinor.
(* Goal: False *)
      destruct Hinor as [ Hin1 | Hin2 ].
      * inversion Hnodup1 as [ | aa ab Hnotin1 ad ae ].
(* Goal: False *)
        exact (Hnotin1 Hin1).
      * revert Hin2.
(* Goal: not (@In A x l2) *)
        apply Hnotin.
(* Goal: @In A x1 (@cons A x1 l1') *)
        apply in_eq.
    + apply IH;
      [ idtac | inversion Hnodup1; assumption | assumption ].
(* Goal: forall (x : A) (_ : @In A x l1'), not (@In A x l2) *)
      intros x Hin.
(* Goal: not (@In A x l2) *)
      apply Hnotin.
(* Goal: @In A x (@cons A x1 l1') *)
      apply in_cons.
(* Goal: not (@In A x l) *)
      assumption.
Qed.

Lemma NoDup_split (A: Type) (l1 l2: list A):
  NoDup (l1 ++ l2) ->
  NoDup l1.
Proof.
(* Goal: forall _ : @NoDup A (@app A l1 l2), @NoDup A l1 *)
  revert l1.
  induction l2 as [ | x2 l2' IH ];
    intros l1 Hnodupapp.

  - rewrite app_nil_r in Hnodupapp.
(* Goal: @NoDup A (@app A l1 (@cons A x2 l2')) *)
    exact Hnodupapp.

  - apply IH.
(* Goal: @NoDup A (@app A l1 l2') *)
    apply NoDup_remove_1 with (a := x2).
(* Goal: @NoDup A (@app A l1 (@cons A x2 l2')) *)
    exact Hnodupapp.
Qed.

Lemma NoDup_split_right : forall (A : Type) (l1 l2 : list A), NoDup (l1 ++ l2) -> NoDup l2.
Proof.
(* Goal: forall (A : Type) (l1 l2 : list A) (_ : @NoDup A (@app A l1 l2)), @NoDup A l2 *)
intro A.
(* Goal: forall (l1 l2 : list A) (_ : @NoDup A (@app A l1 l2)), @NoDup A l2 *)
induction l1; intros l2 H.
- assumption.

- simpl in H.
  change (a :: l1 ++ l2) with ([] ++ a :: l1 ++ l2) in H.
(* Goal: @NoDup A l2 *)
  apply NoDup_remove_1 in H.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
  auto.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Theorem NoDup_cons_iff {A:Type} (a: A) (l: list A):
  NoDup (a::l) <-> ~ In a l /\ NoDup l.
Proof.
(* Prouvé dans stdlib 8.5 *)
(* Goal: iff (@NoDup A (@cons A a l)) (and (not (@In A a l)) (@NoDup A l)) *)
split; intro H.
(* Goal: @NoDup A t1 *)
- inversion H; tauto.
(* Goal: @NoDup A t1 *)
- constructor; tauto.
Qed.

Lemma NoDup_app_in_l A l l' :
  NoDup (l ++ l') -> forall x : A, (In x l) -> ~ (In x l').
Proof.
(* Goal: forall (_ : @NoDup A (@app A l l')) (x : A) (_ : @In A x l), not (@In A x l') *)
revert l'; induction l; intros l' H x Hin.
(* Goal: @NoDup A t1 *)
- tauto.
- simpl in H.
(* Goal: not (@In A x l') *)
  apply NoDup_cons_iff in H.
(* Goal: not (@In A x l') *)
  destruct H as (H & HND).
(* Goal: P x *)
  rewrite in_app_iff in H.
(* Goal: not (@In A x l') *)
  apply Decidable.not_or in H.
(* Goal: @Forall2 A B P la lb *)
  destruct H.
(* Goal: not (@In A x l') *)
  destruct Hin.
  + subst.
(* Goal: not (@In A x l) *)
    assumption.
  + apply IHl; assumption.
Qed.

(* dans la lib standard de coq 8.5 *)
Lemma NoDup_Permutation_NoDup A l l' : @NoDup A l -> Permutation.Permutation l l' -> NoDup l'.
Proof.
(* Goal: forall (_ : @NoDup A l) (_ : @Permutation A l l'), @NoDup A l' *)
  intros NDl Hperm.
(* Goal: @NoDup A l' *)
  induction Hperm.
  - trivial.
  - rewrite <- app_nil_l in NDl.
(* Goal: @NoDup A (@cons A y (@app A (@nil A) l)) *)
    apply NoDup_cons.
    + apply NoDup_remove_2 in NDl.
      simpl  in NDl.
(* Goal: not (@In A x l') *)
      intro H'.
(* Goal: @NoDup A (@app A (@nil A) (@cons A y l)) *)
      apply NDl.
(* Goal: @In A x l *)
      apply Permutation.Permutation_in with l'.
      * auto with *.
      * assumption.
    + apply IHHperm.
(* Goal: @NoDup A (@cons A y l) *)
      apply NoDup_remove_1 in NDl.
(* Goal: @NoDup A (@app A (@nil A) (@cons A y l)) *)
      apply NDl.
  - replace (y :: x :: l) with ([y] ++ x :: l) in NDl by trivial.
(* Goal: @NoDup A (@cons A y (@app A (@nil A) l)) *)
    apply NoDup_cons.
    + apply NoDup_remove_2 in NDl.
(* Goal: @NoDup A (@app A (@nil A) (@cons A y l)) *)
      apply NDl.
    + apply NoDup_remove_1 in NDl.
      replace l with ([]++l) by trivial.
(* Goal: @NoDup A (@cons A y (@app A (@nil A) l)) *)
      apply NoDup_cons.
      * apply NoDup_remove_2.
(* Goal: @NoDup A (@app A (@nil A) (@cons A y l)) *)
        apply NDl.
      * apply NoDup_remove_1 with y.
(* Goal: @NoDup A (@app A (@nil A) (@cons A y l)) *)
        apply NDl.
(* Goal: @NoDup A t1 *)
  - tauto.
Qed.

(* 8.5 : NoDup_incl_length *)
Lemma NoDup_incl_le_length (A: Type)
  (l1 l2: list A):
  NoDup l1 -> incl l1 l2 -> length l1 <= length l2.
Proof.
(* Goal: forall (_ : @NoDup A l1) (_ : @incl A l1 l2), le (@length A l1) (@length A l2) *)
intro Hnd.
(* Goal: forall _ : @incl A l1 l2, le (@length A l1) (@length A l2) *)
revert l2.
(* Goal: forall (l2 : list A) (_ : @incl A l1 l2), le (@length A l1) (@length A l2) *)
induction Hnd; intros l2 Hincl.
  - apply le_0_n.
  - simpl.
(* Goal: le (S (@length A l)) (@length A l2) *)
    assert (In x l2) by apply Hincl, in_eq.
(* Goal: le (S (@length A l)) (@length A l2) *)
    apply in_split in H0.
(* Goal: le (S (@length A l)) (@length A l2) *)
    destruct H0 as (l3 & l4 & Hl2).
(* Goal: le (S (@length A l)) (@length A l2) *)
    subst l2.
(* Goal: le (S (@length A l)) (@length A (@app A l3 (@cons A x l4))) *)
    rewrite app_length.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    simpl.
    rewrite <- plus_n_Sm.
    rewrite <- app_length.
(* Goal: le (S (@length A l)) (S (@length A (@app A l3 l4))) *)
    apply le_n_S.
(* Goal: le (@length A l) (@length A (@app A l3 l4)) *)
    apply IHHnd.
(* Goal: @incl A l (@app A l3 l4) *)
    apply incl_remove_app with x.
    + assumption.
    + apply tl_incl with x; assumption.
Qed.

Lemma NoDup_flat_map A B (f : A -> list B) l :
  (forall x, In x l -> NoDup (f x)) ->
  NoDup l ->
  (forall x y, In x l -> In y l -> x <> y -> (forall z, In z (f x) <-> ~ In z (f y))) ->
  NoDup (flat_map f l).
Proof.
induction l; intros Hf Hl Hmut.
- apply NoDup_nil.

- simpl.
  apply NoDup_app.
  + intros x Hx Hfalse.
     apply in_flat_map in Hfalse.
     destruct Hfalse as (b & Hbl & Hxb).
     eapply (Hmut b a).
     * auto with *.
     * auto with *.
     * inversion Hl.
(* Goal: forall _ : forall (a : A) (_ : @In A a l), @eq bool (f a) (g a), @eq (list A) (@filter A f l) (@filter A g l) *)
        intro Heq.
(* Goal: not (@In A x l') *)
        subst.
(* Goal: @NoDup A t1 *)
        tauto.
     * exact Hxb.
     * assumption.
  + apply Hf.
(* Goal: @NoDup A l *)
    left; trivial.
  + apply IHl.
    * auto with *.
    * inversion Hl.
(* Goal: not (@In A x l) *)
       assumption.
    * auto with *.
Qed.

End NoDup.

(* version dans Set de ListDec.uniquify *)
Definition uniquify A (d : forall a b : A, { a = b} + { a <> b}) (l:list A) : list A :=
list_rect (fun _ : list A => list A) []
  (fun (a : A) (_ l' : list A) => let s := in_dec d a l' in if s then l' else a :: l') l.


Section pow.

Lemma lt_0_pow x n : 0 < x ->  0 < Nat.pow x n.
Proof.
(* Goal: forall _ : lt O x, lt O (Nat.pow x n) *)
  induction n.
  - auto.
  - intro H.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
    simpl.
    rewrite <- (mult_0_r x) at 1.
(* Goal: @NoDup A t1 *)
    apply mult_lt_compat_l; tauto.
Qed.

Lemma pow_le_compat x y n:
  x <= y -> Nat.pow x n <= Nat.pow y n.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros.
(* Goal: @NoDup A l *)
induction n;simpl;try trivial.
(* Goal: @NoDup A t1 *)
apply Mult.mult_le_compat;tauto.
Qed.

End pow.

Lemma length_filter (A B : Type) (c : B -> bool) (f : A -> B) (xs : list A) :
  length (filter (fun x => c (f x)) xs) =
  length (filter c (map f xs)).
Proof.
(* Goal: @NoDup A l *)
induction xs as [ | x xs IH ]; trivial.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
simpl.
(* Goal: @NoDup A l *)
case (c (f x)); trivial.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
simpl; congruence.
Qed.

Section Sublist.

Inductive sublist (A : Type) : (list A) -> (list A) -> Prop :=
| sublist_refl : forall l, sublist l l
| sublist_skip : forall l1 h t, sublist l1 t -> sublist l1 (h :: t)
| sublist_cons : forall h t1 t2, sublist t1 t2 -> sublist (h :: t1) (h :: t2).

Hint Constructors sublist.

Lemma sublist_nil A (l : list A) : sublist [] l.
Proof.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
induction l; auto.
Qed.

Lemma sublist_incl A (l1 l2 : list A) : sublist l1 l2 -> incl l1 l2.
Proof.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: forall (x : A) (_ : @In A x l), @Permutation B (f x) (g x) *)
induction H; intros x Hx.
- trivial.
- right.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
  auto.
- destruct Hx.
  + left; trivial.
  + right; auto.
Qed.

Lemma sublist_app_skip A (l1 l2 l3 : list A) : sublist l1 l3 -> sublist l1 (l2 ++ l3).
Proof.
(* Goal: not (@eq A x y) *)
induction l2; intro H.
- trivial.
- simpl.
(* Goal: @NoDup A t1 *)
  apply sublist_skip; tauto.
Qed.

Lemma sublist_app_left A (l1 l2 l3 : list A) : sublist l1 l3 -> sublist (l2 ++ l1) (l2 ++ l3).
Proof.
(* Goal: not (@eq A x y) *)
induction l2; intro H.
- trivial.
- simpl.
(* Goal: @NoDup A t1 *)
  apply sublist_cons; tauto.
Qed.

Lemma sublist_app_compat A (l1 l2 l3 l4 : list A) :
  sublist l1 l3 -> 
  sublist l2 l4 ->
  sublist (l1 ++ l2) (l3 ++ l4).
Proof.
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
intros H13 H14; induction H13; simpl.
- apply sublist_app_left; trivial.
- apply sublist_skip; trivial.
- apply sublist_cons; trivial.
Qed.

Lemma sublist_flatmap_in_ext A B (f : A -> list B) g l: 
  (forall x : A , In x l -> sublist (f x) (g x)) ->
  sublist (flat_map f l) (flat_map g l).
Proof.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- apply sublist_refl.
- simpl.
  apply sublist_app_compat; auto with *.
Qed.

Lemma NoDup_sublist A (l1 l2 : list A) : sublist l1 l2 -> NoDup l2 -> NoDup l1.
Proof.
(* Goal: forall (_ : @NoDup A l1) (_ : @incl A l1 l2), le (@length A l1) (@length A l2) *)
intro H; induction H; intro Hnd.
- trivial.
(* Goal: @NoDup A t1 *)
- inversion Hnd; tauto.
- inversion Hnd; apply NoDup_cons.
  + apply sublist_incl in H; auto.
(* Goal: @NoDup A t1 *)
  + tauto.
Qed.

End Sublist.

(* lemmes de compatibilité présents dans coq 8.5 *)
Section Compat.

Lemma NoDup_map_inv A B (f:A->B) l : NoDup (map f l) -> NoDup l.
Proof.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
 induction l; simpl; inversion_clear 1; subst; constructor; auto.
(* Goal: not (@eq A x y) *)
 intro H. now apply (in_map f) in H.
Qed.

End Compat.

Lemma In_In_list_decompose {A} (x y : A) l : In x l -> In y l ->
  x = y \/
  exists l1 l2 l3, (l = l1 ++ x :: l2 ++ y :: l3) \/ (l = l1 ++ y :: l2 ++ x :: l3).
Proof.
(* Goal: forall (_ : @In A x l) (_ : @In A y l), or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
intros Hx Hy.
(* Goal: or (@eq A x y) (@ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) l (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) l (@app A l1 (@cons A y (@app A l2 (@cons A x l3))))))))) *)
induction l.
- inversion Hx.
- destruct Hx as [Hx | Hx]; destruct Hy as [Hy | Hy].
  + left; subst; trivial.
  + subst a.
(* Goal: sumbool (@eq A x y) (not (@eq A x y)) *)
    right.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A y l) (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A y l) (@app A l1 (@cons A y (@app A l2 (@cons A x l3)))))))) *)
    exists [].
(* Goal: @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A x l) (@app A (@nil A) (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A x l) (@app A (@nil A) (@cons A y (@app A l2 (@cons A x l3))))))) *)
   apply in_split in Hy.
(* Goal: @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A x l) (@app A (@nil A) (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A x l) (@app A (@nil A) (@cons A y (@app A l2 (@cons A x l3))))))) *)
   destruct Hy as (l2 & l3 & Hy).
(* Goal: @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A y (@app A l2 (@cons A x l3))))))) *)
   exists l2; exists l3.
(* Goal: @NoDup A l *)
   left; simpl; rewrite Hy; trivial.
  + subst a.
(* Goal: sumbool (@eq A x y) (not (@eq A x y)) *)
    right.
(* Goal: @ex (list A) (fun l1 : list A => @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A y l) (@app A l1 (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A y l) (@app A l1 (@cons A y (@app A l2 (@cons A x l3)))))))) *)
    exists [].
(* Goal: @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A y (@app A l2 (@cons A x l3))))))) *)
   apply in_split in Hx.
(* Goal: @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A y (@app A l2 (@cons A x l3))))))) *)
   destruct Hx as (l2 & l3 & Hy).
(* Goal: @ex (list A) (fun l2 : list A => @ex (list A) (fun l3 : list A => or (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A x (@app A l2 (@cons A y l3))))) (@eq (list A) (@cons A y l) (@app A (@nil A) (@cons A y (@app A l2 (@cons A x l3))))))) *)
   exists l2; exists l3.
(* Goal: @NoDup A l *)
   right; simpl; rewrite Hy; trivial.
  + apply IHl in Hx; [| exact Hy].
    destruct Hx as [Heq | (l1 & l2 & l3 & [H | H])]; [tauto | | ]; right;
(* Goal: @NoDup A t1 *)
       exists (a::l1); exists l2; exists l3; rewrite H; tauto.
Qed.

Section Lexicographic_Product.

Variables A B : Type.

Variable ltA : A -> A -> Prop.

Variable ltB : B -> B -> Prop.

Hypothesis wf_ltA : well_founded ltA.

Hypothesis wf_ltB : well_founded ltB.

Inductive lexprod : A*B -> A*B -> Prop :=
| lex_l : forall a a' b b', ltA a a' -> lexprod (a, b) (a', b')
| lex_r : forall a    b b', ltB b b' -> lexprod (a, b) (a,  b').

Lemma acc_lex a b : Acc ltA a -> Acc ltB b -> Acc lexprod (a, b).
Proof.
(* Goal: forall (_ : @Acc A ltA a) (_ : @Acc B ltB b), @Acc (prod A B) lexprod (@pair A B a b) *)
intro HaccA.
(* Goal: forall _ : @Acc B ltB b, @Acc (prod A B) lexprod (@pair A B a b) *)
revert b.
(* Goal: forall (b : B) (_ : @Acc B ltB b), @Acc (prod A B) lexprod (@pair A B a b) *)
induction HaccA as [ a _ IHA ].
intros b  HaccB.
(* Goal: @Acc (prod A B) lexprod (@pair A B a b) *)
induction HaccB as [ b _ IHB ].
(* Goal: @Acc (prod A B) lexprod (@pair A B a b) *)
constructor.
(* Goal: forall (y : prod A B) (_ : lexprod y (@pair A B a b)), @Acc (prod A B) lexprod y *)
intros [a' b'] Hle.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
inversion Hle; auto.
Qed.

Lemma lexprod_trans :
  (forall a1 a2 a3, ltA a1 a2 -> ltA a2 a3 -> ltA a1 a3) ->
  (forall b1 b2 b3, ltB b1 b2 -> ltB b2 b3 -> ltB b1 b3) ->
  forall x1 x2 x3, lexprod x1 x2 -> lexprod x2 x3 -> lexprod x1 x3.
Proof.
(* Goal: forall (_ : forall (a1 a2 a3 : A) (_ : ltA a1 a2) (_ : ltA a2 a3), ltA a1 a3) (_ : forall (b1 b2 b3 : B) (_ : ltB b1 b2) (_ : ltB b2 b3), ltB b1 b3) (x1 x2 x3 : prod A B) (_ : lexprod x1 x2) (_ : lexprod x2 x3), lexprod x1 x3 *)
intros Htrans1 Htrans2 [a1 b1] [a2 b2] [a3 b3] H1 H2.
(* Goal: not (@In A x l') *)
inversion H1; inversion H2; subst.
- left; now apply Htrans1 with a2.
- now left.
- now left.
- right; now apply Htrans2 with b2.
Qed.

Lemma wf_lexprod : well_founded lexprod.
Proof.
(* Goal: @well_founded (prod A B) lexprod *)
intros [a b].
(* Goal: @NoDup A l *)
apply acc_lex; trivial.
Qed.

Definition lex_prod_dec: 
  (forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) ->
  (forall a1 a2, {ltA a1 a2} + {~ltA a1 a2}) ->
  (forall b1 b2, {ltB b1 b2} + {~ltB b1 b2}) ->
  (forall x y, {lexprod x y} + {~ lexprod x y}).
Proof.
(* Goal: forall (_ : forall a1 a2 : A, sumbool (@eq A a1 a2) (not (@eq A a1 a2))) (_ : forall a1 a2 : A, sumbool (ltA a1 a2) (not (ltA a1 a2))) (_ : forall b1 b2 : B, sumbool (ltB b1 b2) (not (ltB b1 b2))) (x y : prod A B), sumbool (lexprod x y) (not (lexprod x y)) *)
intros Heqdec Hdec1 Hdec2 [a1 b1] [a2 b2].
(* Goal: sumbool (lexprod (@pair A B a1 b1) (@pair A B a2 b2)) (not (lexprod (@pair A B a1 b1) (@pair A B a2 b2))) *)
destruct (Hdec1 a1 a2) as [Htrue1 | Hfalse1].
- left.
(* Goal: @NoDup A l *)
  constructor 1; trivial.
- destruct (Heqdec a1 a2) as [Heq | Hneq].
  + destruct (Hdec2 b1 b2) as [Htrue2 | Hfalse2]; subst.
    * left; constructor 2; trivial.
(* Goal: sumbool (@eq A x y) (not (@eq A x y)) *)
    * right.
(* Goal: not (lexprod (@pair A B a2 b1) (@pair A B a2 b2)) *)
       contradict Hfalse2.
(* Goal: @NoDup A t1 *)
       inversion Hfalse2; tauto.
  + right.
(* Goal: not (lexprod (@pair A B a1 b1) (@pair A B a2 b2)) *)
    contradict Hfalse1.
(* Goal: @NoDup A t1 *)
    inversion Hfalse1; tauto.
Defined.

End Lexicographic_Product.

Section Last.

Lemma non_empty_last (A:Type) d d' (l:list A):
  l <> [] -> (last l d) = (last l d').
Proof.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
intro. induction l; try destruct l.
- intuition.
- simpl. auto.
- replace (last (a :: a0 :: l) d) with (last (a0 :: l) d).
(* Goal: @eq A (@last A (@cons A a0 l) d) (@last A (@cons A a (@cons A a0 l)) d') *)
(* Goal: @eq A (@last A (@cons A a0 l) d) (@last A (@cons A a (@cons A a0 l)) d) *)
  replace (last (a :: a0 :: l) d') with (last (a0 :: l) d').
  + apply IHl. discriminate.
  + simpl. auto.
  + simpl. auto.
Qed.

Lemma cons_cons_last (A:Type) (a b:A) l x:
  last (a::b::l) x = last (b::l) x.
Proof. simpl. auto. Qed.

Lemma cons_last (A:Type) (a:A) l x:
  last (a::l) x = last l a.
Proof. 
(* Goal: @eq A (@last A (@cons A a (@cons A b l)) x) (@last A (@cons A b l) x) *)
destruct l; try now simpl. rewrite cons_cons_last. apply non_empty_last. discriminate.
Qed.

Lemma last_in (A:Type) (l:list A) x:
  (last l x = x) \/ (In (last l x) l).
Proof.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
induction l; try destruct l; try rewrite cons_cons_last; try destruct IHl; simpl; auto.
Qed.

End Last.

Lemma beq_eq_dec {A : Type} {beq : A -> A -> bool} (Hbeq : forall x y, beq x y = true <-> x = y) : forall (x y : A), {x = y} + {~ x = y}.
Proof.
(* Goal: forall x y : A, sumbool (@eq A x y) (not (@eq A x y)) *)
intros x y.
(* Goal: sumbool (@eq A x y) (not (@eq A x y)) *)
assert (Heq := Hbeq x y).
(* Goal: @NoDup A t1 *)
destruct (beq x y); try tauto.
(* Goal: sumbool (@eq A x y) (not (@eq A x y)) *)
right.
(* Goal: not (@eq A x y) *)
intro H.
(* Goal: False *)
inversion Heq.
auto with *.
Qed.

Section Firstn_skipn.
Lemma firstn_map {A B : Type} (f : A -> B) l n : 
  firstn n (map f l) = map f (firstn n l).
Proof.
(* Goal: @eq (list B) (@skipn B n (@map A B f l)) (@map A B f (@skipn A n l)) *)
revert l.
(* Goal: @NoDup A l *)
induction n; simpl; trivial.
(* Goal: forall l : list A, @eq (list B) match @map A B f l with | nil => @nil B | cons a l0 => @skipn B n l0 end (@map A B f match l with | nil => @nil A | cons a l0 => @skipn A n l0 end) *)
destruct l; simpl; trivial; now rewrite IHn.
Qed.

Lemma skipn_map {A B : Type} (f : A -> B) l n : 
  skipn n (map f l) = map f (skipn n l).
Proof.
(* Goal: @eq (list B) (@skipn B n (@map A B f l)) (@map A B f (@skipn A n l)) *)
revert l.
(* Goal: @NoDup A l *)
induction n; simpl; trivial.
(* Goal: forall l : list A, @eq (list B) match @map A B f l with | nil => @nil B | cons a l0 => @skipn B n l0 end (@map A B f match l with | nil => @nil A | cons a l0 => @skipn A n l0 end) *)
destruct l; simpl; trivial; now rewrite IHn.
Qed.

Lemma skipn_app_length {A : Type} (l1 l2 : list A) : skipn (length l1) (l1 ++ l2) = l2.
Proof.
(* Goal: @eq (list A) (@filter A f (@app A l1 l2)) (@app A (@filter A f l1) (@filter A f l2)) *)
now induction l1.
Qed.

Lemma firstn_app_length {A : Type} (l1 l2 : list A) : firstn (length l1) (l1 ++ l2) = l1.
Proof.
(* Goal: @NoDup A l *)
induction l1; trivial.
(* Goal: @eq (list A) (@firstn A (@length A (@cons A a l1)) (@app A (@cons A a l1) l2)) (@cons A a l1) *)
simpl; now rewrite IHl1.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma skipn_nil : forall {A} n (x : list A),
  length x <= n -> skipn n x = nil.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
  induction n; simpl in *; trivial; intros.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
  apply length_nil; auto; omega.
  destruct x; simpl in *; trivial.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
  apply IHn; omega.
Qed.

Lemma firstn_seq n start len :
  firstn n (seq start len) = seq start (min n len).
Proof.
(* Goal: @eq (list nat) (@skipn nat n (seq start len)) (seq (Init.Nat.add start n) (Init.Nat.sub len n)) *)
 intros; revert n start.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
 induction len; simpl; intros.
(* Goal: @eq (list nat) (@firstn nat n (@nil nat)) (seq start (Init.Nat.min n O)) *)
(* Goal: @eq (list nat) (@firstn nat n (@cons nat start (seq (S start) len))) (seq start (Init.Nat.min n (S len))) *)
 rewrite min_r; simpl;[ | omega].
(* Goal: @eq (list nat) (@firstn nat n (@nil nat)) (@nil nat) *)
(* Goal: @eq (list nat) (@firstn nat n (@cons nat start (seq (S start) len))) (seq start (Init.Nat.min n (S len))) *)
 apply firstn_nil.
(* Goal: forall _ : @eq nat x1 x2, @eq nat (Init.Nat.add x1 y) (Init.Nat.add x2 y) *)
 case n; simpl; trivial; congruence.
Qed.

Lemma skipn_seq n start len :
  skipn n (seq start len) = seq (start+n) (len-n).
Proof.
(* Goal: @eq (list nat) (@skipn nat n (seq start len)) (seq (Init.Nat.add start n) (Init.Nat.sub len n)) *)
 intros; revert n start.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
 induction len; simpl; intros.
(* Goal: not (and (le a (Init.Nat.add a b)) (lt (Init.Nat.add a b) (Init.Nat.add a b))) *)
 apply skipn_nil; simpl; omega.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
 case n; simpl; intros.
(* Goal: @NoDup A l *)
 rewrite plus_0_r; trivial.
 rewrite <- plus_Snm_nSm; apply IHlen.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma skipn_firstn {A:Type} n (l:list A):
  skipn n (firstn n l) = [].
Proof. apply skipn_nil. apply firstn_le_length. Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma skipn_incl {A:Type} (l:list A) n:
  incl (skipn n l) l.
Proof.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
generalize (firstn_skipn n l). intro.
rewrite <- H at 2. unfold incl. intros.
(* Goal: sumbool (@eq A x y) (not (@eq A x y)) *)
rewrite in_app_iff. now right.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma skipn_app2 {A : Type} (l l' : list A) n:
  length l = n → skipn n (l ++ l') = l'.
Proof. intro. rewrite <- H. apply skipn_app_length. Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma firstn_app {A} (l l' : list A) : 
  firstn (length l) (l ++ l') = l.
Proof.
(* Goal: @NoDup A l *)
 induction l; intros; simpl; trivial.
(* Goal: @NoDup A l *)
 rewrite IHl; trivial.
Qed.

Lemma firstn_app2 : forall (A : Type) (l l' : list A) n, 
 length l = n -> firstn n (l ++ l') = l .
Proof. intros; subst; apply firstn_app. Qed.
End Firstn_skipn.

Section Ints.
Definition ints (n m:nat):list nat := seq n (m-n). (* [n; … ; m-1] *)
Lemma ints_bounded : ∀ (x n m:nat),
  n ≤ m → x ∈ (ints n m) → n ≤ x < m.
Proof. unfold ints. intros. rewrite in_seq in H0. intuition. Qed.

Lemma ints_bounds : ∀ (x n m:nat),
  n ≤ x < m → x ∈ (ints n m).
Proof. unfold ints. intros. rewrite in_seq. intuition. Qed.

Lemma ints_bounds_iff: ∀ x n m,
  n ≤ m → (n ≤ x < m ↔ x ∈ (ints n m)).
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros. split; auto using ints_bounds, ints_bounded.
Qed.

Lemma ints_length : ∀ n m,
  n ≤ m → length (ints n m) = m-n.
Proof. unfold ints. intros. now rewrite seq_length. Qed.
End Ints.

Section Forall.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall_cons_iff {A:Type} (x:A) (xs:list A) (P:A→Prop):
  Forall P (x::xs) ↔ P x ∧ Forall P xs.
Proof. repeat rewrite Forall_forall. intuition. simpl in H. destruct H; auto. now subst x0. Qed.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall_map_iff {A B:Type} (f: A → B) l (P: B → Prop):
  (∀ x, x ∈ l → P (f x)) ↔ Forall P (map f l).
Proof.
(* Goal: iff (forall (x : A) (_ : @In A x (@cons A a (@nil A))), P x) (P a) *)
rewrite Forall_forall. intuition.
- rewrite in_map_iff in H0. repeat destruct H0. now apply H.
- apply H. now apply in_map.
Qed.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall_app_iff {A:Type} (P:A→Prop) l1 l2:
  Forall P (l1++l2) ↔ Forall P l1 ∧ Forall P l2.
Proof.
(* Goal: iff (forall (x : A) (_ : @In A x (@cons A a (@nil A))), P x) (P a) *)
repeat rewrite Forall_forall. intuition. rewrite in_app_iff in H.
(* Goal: P x *)
destruct H; [now apply H0 | now apply H1].
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall_unary {A:Type} (P:A→Prop) a:
  Forall P [a] ↔ P a.
Proof. rewrite Forall_forall. intuition. simpl in H0. now repeat destruct H0. Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall_flat_map {A B:Type} (P:B → Prop) (f:A → list B) l:
  Forall P (flat_map f l) ↔ Forall (λ x, Forall P (f x)) l.
Proof.
(* Goal: iff (@Forall B P (@flat_map A B f l)) (@Forall A (fun x : A => @Forall B P (f x)) l) *)
induction l; simpl; split; intros; try apply Forall_nil.
- rewrite Forall_app_iff in H. destruct H.
  apply Forall_cons; auto. now rewrite <- IHl.
- rewrite Forall_app_iff. rewrite Forall_cons_iff in H. destruct H.
(* Goal: @eq nat (if eq_dec a0 a then S (@count_occ A eq_dec (@app A l l') a) else @count_occ A eq_dec (@app A l l') a) (Init.Nat.add (if eq_dec a0 a then S (@count_occ A eq_dec l a) else @count_occ A eq_dec l a) (@count_occ A eq_dec l' a)) *)
  split; auto. now rewrite IHl.
Qed.
End Forall.

Section Concat.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma concat_unary_is_map {A B:Type}: ∀ l (f:A→B),
  concat (map (λ x, [f x]) l) = map f l.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros. induction l; simpl; auto. now rewrite IHl.
Qed.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma in_concat_const_is_in {A B:Type} (a:A) lfix l:
  a ∈ concat (map (λ _ : B, lfix) l) ↔ l ≠ [] ∧ a ∈ lfix.
Proof.
(* Goal: @NoDup A t1 *)
induction l; simpl; try tauto. intuition; try discriminate.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
rewrite in_app_iff in H0. destruct H0; auto. now apply H.
Qed.
End Concat.

Section Incl.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma incl_nil {A:Type} (l:list A): incl [] l.
Proof. unfold incl. now simpl. Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma incl_map_flat_map {A B:Type} (xs:list A) (f:A → B) g:
  (∀ x : A, x ∈ xs → f x ∈ g x) →
  incl (map f xs) (flat_map g xs).
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
unfold incl. intros.
(* Goal: @ex A (fun x : A => and (@In A x xs) (@In C a (lh x))) *)
rewrite in_map_iff in H0. rewrite in_flat_map.
(* Goal: le (f m) n *)
repeat destruct H0. eauto.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma incl_flat_map_incl {A B C:Type} (xs:list A) (r:A→list B) (rh:B→list C) lh:
  (∀ x : A, x ∈ xs → incl (flat_map rh (r x)) (lh x)) →
  incl (flat_map rh (concat (map r xs))) (flat_map lh xs).
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
unfold incl. intros.
(* Goal: le (f m) n *)
rewrite in_flat_map in *. repeat destruct H0.
(* Goal: le (f m) n *)
rewrite in_concat_iff in H0. repeat destruct H0.
(* Goal: le (f m) n *)
rewrite in_map_iff in H0. repeat destruct H0.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
exists x1. split; auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
apply H; auto.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
rewrite in_flat_map. eauto.
Qed.
End Incl.

Section Append.
(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma app_length_eq {A:Type}:
  ∀ (l1 l2 l1' l2': list A),
  length l1 = length l1' → (l1++l2) = (l1'++l2') →
  l1 = l1' ∧ l2 = l2'.
Proof.
(* Goal: forall (_ : @eq nat (@length A la1) (@length B lb1)) (_ : @Forall2 A B P (@app A la1 la2) (@app B lb1 lb2)), and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
induction l1; intros.
- simpl in *. symmetry in H. rewrite length_zero_iff_nil in H.
  now rewrite H in *.
- destruct l1'.
  + simpl in H. discriminate.
  + simpl in *. inversion H. inversion H0.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
    generalize (IHl1 l2 l1' l2' H2 H4). intro.
(* Goal: and (@eq (list A) (@cons A a0 l1) (@cons A a0 l1')) (@eq (list A) l2 l2') *)
    destruct H1. split; auto.
(* Goal: @eq (list A) (@cons A a0 l1) (@cons A a0 l1') *)
    now rewrite H1.
Qed.
End Append.

Section Forall2.
Lemma Forall2_le_refl l: Forall2 le l l.
Proof. induction l; simpl; auto. Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall2_app_inv {A B:Type} (P:A→B→Prop) la1 la2 lb1 lb2:
  length la1 = length lb1 → Forall2 P (la1++la2) (lb1++lb2) →
  Forall2 P la1 lb1 ∧ Forall2 P la2 lb2.
Proof.
(* Goal: and (@Forall2 A B P la1 lb1) (@Forall2 A B P la2 lb2) *)
intros. split.
- generalize (Forall2_app_inv_l la1 la2 H0). intro.
(* Goal: and (@eq (list A) (@cons A a0 l1) (@cons A a0 l1')) (@eq (list A) l2 l2') *)
  do 3 destruct H1. destruct H2.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
  generalize (Forall2_length H1). rewrite H. intro.
(* Goal: @Forall2 A B P la1 lb1 *)
  generalize (app_length_eq lb1 lb2 x x0 H4 H3).
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
  intro. now repeat destruct H5.
- generalize (Forall2_app_inv_r lb1 lb2 H0). intro.
(* Goal: and (@eq (list A) (@cons A a0 l1) (@cons A a0 l1')) (@eq (list A) l2 l2') *)
  do 3 destruct H1. destruct H2.
  generalize (Forall2_length H1). rewrite <- H. intro.
(* Goal: @Forall2 A B P la2 lb2 *)
  symmetry in H4.
(* Goal: @Forall2 A B P la2 lb2 *)
  generalize (app_length_eq la1 la2 x x0 H4 H3).
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
  intro. repeat destruct H5. now rewrite H6.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall2_firstn {A B:Type} (P:A→B→Prop) la lb n:
  Forall2 P la lb → Forall2 P (firstn n la) (firstn n lb).
Proof.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
intro. generalize (Forall2_length H). intro.
rewrite <- (firstn_skipn n) in H.
rewrite <- (firstn_skipn n la) in H.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
apply (Forall2_app_inv (firstn n la) (skipn n la) (firstn n lb) (skipn n lb)); auto.
(* Goal: @eq (option V) (@assoc K V beq k (@app (prod K V) l1 l2)) (@assoc K V beq k l1) *)
repeat rewrite firstn_length. now rewrite H0.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall2_skipn {A B:Type} (P:A→B→Prop) la lb n:
  Forall2 P la lb → Forall2 P (skipn n la) (skipn n lb).
Proof.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
intro. generalize (Forall2_length H). intro.
rewrite <- (firstn_skipn n) in H.
rewrite <- (firstn_skipn n la) in H.
(* Goal: @eq A match l with | nil => b | cons a0 l0 => @last A l x end match l with | nil => b | cons a0 l0 => @last A l x end *)
apply (Forall2_app_inv (firstn n la) (skipn n la) (firstn n lb) (skipn n lb)); auto.
(* Goal: @eq (option V) (@assoc K V beq k (@app (prod K V) l1 l2)) (@assoc K V beq k l1) *)
repeat rewrite firstn_length. now rewrite H0.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall2_firstn_skipn_iff {A B:Type} (P:A→B→Prop) la lb n:
  Forall2 P la lb ↔ Forall2 P (firstn n la) (firstn n lb) ∧ Forall2 P (skipn n la) (skipn n lb).
Proof.
(* Goal: iff (@Forall2 A B P la lb) (and (@Forall2 A B P (@firstn A n la) (@firstn B n lb)) (@Forall2 A B P (@skipn A n la) (@skipn B n lb))) *)
split; auto using Forall2_firstn, Forall2_skipn.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
intro. destruct H.
rewrite <- (firstn_skipn n). rewrite <- (firstn_skipn n la).
(* Goal: @Forall2 A B P (@app A (@firstn A n la) (@skipn A n la)) (@app B (@firstn B n lb) (@skipn B n lb)) *)
now apply Forall2_app.
Qed.

(* Goal: and (le a n) (lt n (Init.Nat.add a b)) *)
Lemma Forall2_tail {A B:Type} (P:A→B→Prop) la lb:
  Forall2 P la lb → Forall2 P (tl la) (tl lb).
Proof.
(* Goal: forall _ : @eq nat (@length A la) (@length B lb), @Forall2 A B P (@tl A la) (@tl B lb) *)
intro. generalize (Forall2_length H). intro.
destruct la, lb; simpl in *; try discriminate; auto.
(* Goal: and (@eq (list A) (@cons A a l1) (@cons A a0 l1')) (@eq (list A) l2 l2') *)
now inversion H.
Qed.
End Forall2.
