proposition: Lemma sort_le_app : forall l1 l2, sort le l1 -> sort le l2 -> (forall x y, In x l1 -> In y l2 -> le x y) -> sort le (l1 ++ l2).
proof: Proof. induction l1; simpl in *; intuition auto. inversion_clear H. constructor; auto. apply InfA_app; auto. destruct l2; auto. constructor ; auto. auto with datatypes. Qed.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia Coq.Lists.SetoidList Coq.Sorting.Sorting Coq.Sorting.Permutation Coq.Sorting.PermutSetoid Bool EquivDec Permutation