proposition: Lemma Partition_In m m1 m2 k : Partition m m1 m2 -> In k m -> {In k m1}+{In k m2}.
proof: Proof. intros Hm Hk. destruct (In_dec m1 k) as [H|H]; [left|right]; auto. destruct Hm as (Hm,Hm'). destruct Hk as (e,He); rewrite Hm' in He; destruct He. elim H; exists e; auto. exists e; auto. Defined.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)