proposition: Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m).
proof: Proof. induction m. simpl; intuition. intros. destruct a as (x',e'). simpl; case (compare x x'); intuition; inversion_clear Hm; auto with smtcoq_array. constructor; auto with smtcoq_array. apply Inf_eq with (x',e'); auto with smtcoq_array. Qed.
imports: Bool OrderedType SMT_classes ProofIrrelevance