proposition: Lemma sorted_SCC' : {m : list nat | sort RT m & permutation eq_nat_dec (nats_decr_lt dim) m}.
proof: Proof. unfold RT. destruct topo_sortable_Rquo' as [F HF]; simpl. set (RTb := fun x y : N dim => F (nats_decr_lt dim) x y = true) in *. cut ({m : list (N dim) | sort RTb m & permutation N_eq_dec (L dim) m}). intro. destruct H as [mb]. exists (map N_val mb). apply sort_map_N_val. intuition. unfold permutation in *. unfold meq in *. intros. rewrite multiplicity_nats_decr_lt in *. destruct (lt_ge_dec a dim). ded (p (N_ l)). rewrite <- multiplicity_map_N_val, map_N_val_L, multiplicity_nats_decr_lt in H. destruct (lt_ge_dec a dim); try lia. rewrite <- multiplicity_map_N_val in H; auto. erewrite <- multiplicity_map_N_val_notin; auto. cut({m : list (N dim) | sort (RTb %) m & permutation N_eq_dec (L dim) m}). intro. destruct H as [mb]. exists mb; auto. apply nodup_sort_strict; auto. eapply multiplicity_nodup. intros. unfold permutation in *. unfold meq in *. rewrite <- p, multiplicity_L. refl. apply treesort. ded (HF (nats_decr_lt dim)). destruct H; intuition. intros. unfold total in H4. destruct x as [x xdim]. destruct y as [y ydim]. assert (trichotomy (fun x y => F (nats_decr_lt dim) x y = true) x y). apply H4; rewrite <- In_nats_decr_lt; auto. unfold trichotomy in H3. destruct (eq_nat_dec x y). left; left; subst x; auto. f_equal. apply lt_unique. assert ({F (nats_decr_lt dim) x y = true} +{~F (nats_decr_lt dim) x y = true}). destruct (F (nats_decr_lt dim) x y); auto. destruct H5. left; auto. right; auto. right; auto. right; tauto. apply rc_trans. intros x y z xy yz. unfold RTb in *. ded (HF (nats_decr_lt dim)). destruct H. intuition. unfold transitive in *. eapply H0; eauto. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)