proposition: Lemma L5 : forall k b i j, reachable (quad (f b) i (k+j) 0) -> reachable (quad (f (k+b)) i j 0).
proof: Proof. induction k. simpl. auto. intros; econstructor 3. unfold reachable in IHk; eapply IHk. replace (S k + j) with (k + (S j)) in H. unfold reachable in H;eauto. omega. simpl;rewrite f_Sn. apply L3. Qed.
imports: Arith Omega Relations