proposition: Lemma try_add_arc_one_to_many_trichotomy : eq_midex A -> rel_midex R -> forall x y l l', In y l' -> In x l -> incl l' l -> is_restricted R l -> trichotomy (try_add_arc_one_to_many x l') x y.
proof: Proof. induction l'; simpl; intros. contr. pose (incl_cons_l_incl H3). apply trichotomy_preserved with (try_add_arc (try_add_arc_one_to_many x l') x a). apply incl_tc. refl. destruct H1. rewrite H1. apply try_add_arc_trichotomy. hyp. apply try_add_arc_one_to_many_midex with l; hyp. apply trichotomy_preserved with (try_add_arc_one_to_many x l'). apply sub_rel_try_add_arc. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)