proposition: Lemma SortA_app_iff (l1 l2 : list A) : sort ltA (l1++l2) <-> sort ltA l1 /\ sort ltA l2 /\ forall a1 a2, In a1 l1 -> In a2 l2 -> ltA a1 a2.
proof: Proof. split. { induction l1 as [|a1 l1 IHl1]. - easy. - simpl. inversion_clear 1 as [ | ? ? Hs Hhd ]. destruct (IHl1 Hs) as (H1 & H2 & H3); clear IHl1. repeat split. * constructor; auto. destruct l1; simpl in *; auto; inversion_clear Hhd; auto. * trivial. * intros b1 b2 [->|Hb1] Hb2; eauto. eapply SortA_InfA_InA with (eqA:=eqA)(l:=l1++l2); auto. rewrite InA_app_iff. right. apply In_InA; auto with *. } { intros (U & V & W); eapply SortA_app; eauto. intros x y. rewrite !InA_alt. intros (x' & -> & Hx) (y' & -> & Hy); auto. } Qed.
imports: Coq(List SetoidList)