proposition: Lemma iter_le2_spec : forall n x y, iter_le2 n x y <-> exists p, p <= n /\ iter p x y.
proof: Proof. intro. induction n. intros; simpl in *; split; intros. exists 0; split; auto with *. destruct H as [p]; destruct H; assert(p=0); auto with *. subst; auto with *. split; intros; simpl in *. unfold compose in H; destruct H. destruct H as [z]; destruct H; rewrite IHn in H0; destruct H0 as [p]; exists (S p). split; auto with *. simpl; unfold compose; exists z; intuition; auto with *. rewrite IHn in H; destruct H as [p]; exists p; intuition; auto with *. destruct H as [p]; destruct H. destruct (le_lt_eq_dec H). right; apply NatCompat.lt_n_Sm_le in l; rewrite IHn; exists p; auto with *. subst; left; unfold compose in H0; auto with *. simpl in H0; unfold compose in *; destruct H0 as [z]; exists z. split; destruct H0; auto with *. rewrite IHn; exists n; auto. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)