proposition: Lemma dissect_not_nil : forall n l, dissect n l <> nil.
proof: Proof. intros n; destruct l as [|i l]; intros Heq; simpl in Heq; [| destruct (Nat.eqb n i); [| destruct (dissect n l) ]]; discriminate Heq. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)