proposition: Lemma try_add_arc_many_to_many_trichotomy : eq_midex A -> rel_midex R -> forall x y l l', is_restricted R l -> incl l' l -> In y l -> In x l' -> trichotomy (try_add_arc_many_to_many l' l) x y.
proof: Proof. induction l'; simpl; intros. contr. pose (incl_cons_l_incl H2). destruct H4. rewrite H4. apply try_add_arc_one_to_many_trichotomy with l; try hyp. apply try_add_arc_many_to_many_midex; hyp. rewrite <- H4. apply H2. simpl. tauto. refl. apply restricted_try_add_arc_many_to_many; hyp. apply trichotomy_preserved with (try_add_arc_many_to_many l' l). apply sub_rel_try_add_arc_one_to_many. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)