Update

src/permutations.v

@@ -2,6 +2,7 @@ Require Import Nat.
 Require Import PeanoNat.
 Require Import List.
 Require Import Lia.
+Require Import Arith.Factorial.
 Import ListNotations.
 
 (*
@@ -14,6 +15,12 @@ Definition permutation (l: list nat) :=
   forall k:nat, k < List.length l -> In k l.
 
 
+Example example_0: permutation [].
+Proof.
+  unfold permutation. intro k. simpl. easy.
+Qed.
+
+
 Theorem perm_seq_1 : forall (l: list nat),
   permutation l -> incl (seq 0 (length l)) l.
 Proof.
@@ -200,10 +207,43 @@ Proof.
 Qed.
 
 
+Lemma perm_max_insert_alt_2 : forall (l1 l2: list nat),
+  Add (length l1) l1 l2 -> permutation l2
+  -> permutation l1.
+Proof.
+  intros l1 l2. intros H I.
+  apply Add_split in H. destruct H. destruct H. destruct H.
+  rewrite H0 in I. rewrite H. apply perm_max_insert.
+  simpl. rewrite H in I. assumption.
+Qed.
+
+
+Lemma perm_count : forall (n: nat) (E: list (list nat)),
+  NoDup E -> (forall l, In l E <-> (length l = n /\ permutation l))
+  -> length E = fact n.
+Proof.
+  intro n. induction n; intro E; intros H1 H2. simpl.
+
+  assert (I: length (nil: list nat) = 0 /\ permutation nil).
+  easy. apply H2 in I.
+
+   apply In_nth with (d := nil) in I.
+  destruct I. destruct (length E). destruct H.
+  apply Nat.nlt_0_r in H. contradiction H.
+  destruct n. reflexivity. destruct H.
+
+  assert (J: 0 < length E). apply In_nth with (d := nil) in I.
+  destruct I. destruct (length E). destruct H.
+  apply Nat.nlt_0_r in H. contradiction H.
+  apply Arith_prebase.gt_Sn_O_stt.
+
+  assert (K: length E
 
 
 
 
+
+  (*
 Example test1: permutation [1;2;3;0].
 Proof.
   unfold permutation.
@@ -222,9 +262,4 @@ Proof.
   right. right. right. left. easy.
   left. easy. right. left. easy. right. right. left. easy.
 Qed.
-
-
-Example test2: permutation [].
-Proof.
-  unfold permutation. intro k. simpl. easy.
-Qed.
+   *)