proposition: Lemma trans_bpath_try_add_arc : eq_midex A -> forall x y z n, transitive R -> bpath (try_add_arc x y ) n z z -> R z z.
proof: Proof. intros. induction n. inversion H1. destruct l. simpl in H2. apply trans_try_add_arc_sym with x y z; hyp. simpl in H1. pose (Nat.nle_succ_0 (length l) H2). contr. apply IHn. inversion H1. clear IHn H1 H4 H5 x0 y0. destruct (path_nodup_length (try_add_arc x y) H z l z H3). decompose [and] H1. assert (length x0 <= S n). apply Nat.le_trans with (length l); hyp. clear H1 H2 H3 H6 H7 H8. destruct x0. exists (nil : list A). apply Nat.le_0_l. tauto. destruct x0; simpl in * |- . exists (nil : list A). apply Nat.le_0_l. simpl. apply sub_rel_try_add_arc. apply trans_try_add_arc_sym with x y a; tauto. destruct H10. destruct H2. inversion H1; inversion H2. exists (a0::x0). simpl. apply le_S_n. hyp. simpl. split. apply (sub_rel_try_add_arc). apply H0 with a; hyp. hyp. absurd (R a0 a). tauto. apply trans_tc_incl. hyp. apply path_clos_trans with (x0++(z::nil)). apply path_app. apply path_try_add_arc_path with x y. rewrite H13. tauto. hyp. simpl. hyp. absurd (R a z). tauto. apply trans_tc_incl. hyp. apply path_clos_trans with (a0::x0). split. hyp. apply path_try_add_arc_path with x y. rewrite H10. tauto. hyp. rewrite H8 in H13. tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)