proposition: Lemma sorted_app_inv l1 l2 : sort X.lt (l1++l2) -> sort X.lt l1 /\ sort X.lt l2 /\ forall x1 x2, InA X.eq x1 l1 -> InA X.eq x2 l2 -> X.lt x1 x2.
proof: Proof. induction l1 as [|a1 l1 IHl1]. - simpl; repeat split; auto. intros. now rewrite InA_nil in *. - simpl. inversion_clear 1 as [ | ? ? Hs Hhd ]. destruct (IHl1 Hs) as (H1 & H2 & H3). repeat split. * constructor; auto. destruct l1; simpl in *; auto; inversion_clear Hhd; auto. * trivial. * intros x1 x2 Hx1 Hx2. rewrite InA_cons in Hx1. destruct Hx1. + rewrite H. apply SortA_InfA_InA with (eqA:=X.eq)(l:=l1++l2); auto_tc. rewrite InA_app_iff; auto_tc. + auto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat