proposition: Lemma iter_le_fast_spec : forall n x y, iter_le_fast n x y <-> exists p,(S p) <= exp2 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 *. destruct H. destruct H as [z]; destruct H. rewrite IHn in H0; rewrite IHn in H. destruct H0 as [p]; destruct H as [p']; destruct H0; destruct H. exists (p+p'+1). split. lia. assert ((iter p' @ iter p) x y). unfold compose; exists z; auto with *. assert (p+p'+1=p'+p+1); intuition. rewrite H4; apply iter_compose; auto with *. rewrite IHn in H; destruct H as [p]; exists p; intuition. destruct H as [p]; destruct H; simpl in H. destruct (le_gt_dec (S p) (exp2 n)). right; rewrite IHn; exists p; split; auto with *. assert(p = (exp2 n - 1) + (p - exp2 n) +1 ). lia. rewrite H1 in H0. ded (iter_plus_1 _ _ _ _ H0). left; unfold compose in *; destruct H2 as [z]; destruct H2. exists z; split; rewrite IHn. exists (exp2 n -1); intuition; lia. exists (p -exp2 n); intuition; lia. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)