proposition: Lemma sort_aux_equiv : forall l a n, equiv (cons a n l) (sort_aux a n l).
proof: Proof. induction l ; auto with T1. intros x n0; simpl. case (trichotomy_inf x l1). destruct s. eapply equiv_trans. 2:eapply equiv_cons. apply equiv_perm. apply equiv_refl. auto. subst l1. 2:intro;apply equiv_refl. unfold equiv;simpl. intro o;case (T1_eq_dec o x). intro; omega. auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0