proposition: Lemma antisym_topo_sortable_rel_dec : forall R, rel_midex R -> antisym_topo_sortable R -> rel_dec R.
proof: Proof. unfold antisym_topo_sortable, linear_extension. intros R H H0. assert (irreflexive (clos_trans R)). apply local_global_acyclic. intro. exists (fun x y => (let (f,s):= H0 in f) l x y=true). destruct H0. destruct a. pose (H1 l). tauto. assert (eq_dec A). apply total_order_eq_dec. exists (let (f,s):= H0 in f). intro. destruct H0. destruct a. pose (H2 l). split; tauto. do 2 intro. destruct (X x y). rewrite e. constructor 2. intro. apply (H1 y). constructor. hyp. destruct H0. destruct a. pose (H0 x y). decompose [and] (H2 (x::y::nil)). destruct (sumbool_of_bool (x0 (x::y::nil) x y)). destruct (sumbool_of_bool (x0 (y::x::nil) x y)). constructor. destruct (H x y). hyp. destruct (H y x). absurd (x0 (x :: y :: nil) y x=true). intro. apply (H6 x). apply H4 with y; hyp. apply H5. unfold restriction. simpl. tauto. generalize n0 e e0. case (x0 (x :: y :: nil) x y); case (x0 (y :: x :: nil) x y); tauto. constructor 2. intro. absurd (x0 (y :: x :: nil) x y=true). intro. rewrite e0 in H9. inversion H9. pose (H2 (y::x::nil)). decompose [and] a. apply H11. unfold restriction. simpl. tauto. constructor 2. intro. absurd (x0 (x::y:: nil) x y=true). intro. rewrite e in H9. inversion H9. apply H5. unfold restriction. simpl. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)