proposition: Lemma sort_aux_nf : forall (l x:T1) n, nf x -> nf l -> nf (sort_aux x n l).
proof: Proof. induction 2. simpl. auto with T1. simpl. case (trichotomy_inf x a). destruct s. constructor;auto. constructor; auto with T1. constructor; auto with T1 arith. constructor; auto with T1 arith. simpl. case (trichotomy_inf x a). destruct s. simpl in IHnf2. generalize IHnf2. case (trichotomy_inf x a'). destruct s. constructor 3. auto. auto. auto. subst x. constructor;auto. constructor;auto. constructor;auto. constructor. auto. auto. constructor;auto. Qed.
imports: Arith Omega ArithRing More_nat EPSILON0