proposition: Lemma bpath_iter_le : forall n x y, bpath R n x y -> iter_le n x y.
proof: Proof. intro; induction n; intros; simpl in *. inversion H; subst; destruct l; simpl in *; auto with *; inversion H0. gen (bpath_Sn_n_or_Rn H); intros; destruct H0. simpl in *; right; apply IHn; auto with *. destruct H0 as [z]; destruct H0; ded (IHn _ _ H1). simpl; rewrite iter_le_spec in *; destruct H2 as [p]; destruct H2. destruct (le_lt_eq_dec H2). right; rewrite iter_le_spec; exists (S p); intuition. simpl; unfold compose; exists z; intuition. left; subst; unfold compose; exists z; intuition. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)