proposition: Lemma dissect_in : forall l i, In i l -> exists m1 : list nat, exists m2 : list nat, exists mm : list (list nat), m1 :: m2 :: mm = dissect i l.
proof: Proof. induction l; simpl; intros; [ contradiction H | destruct H ]; [ rewrite H; rewrite Nat.eqb_refl; destruct l; simpl; [| destruct (Nat.eqb i n); [| destruct (dissect i l) ]] | destruct (IHl i H) as [m1 [m2 [mm Hm]]]; rewrite <- Hm; destruct (Nat.eqb i a) ]; eexists; eexists; eexists; eauto. Qed.
imports: Coq(Setoid List Relations Wellfounded PeanoNat) CoLoR(weaved_relation list_permut terminaison)