I don't know how to prove a simple theorem used with fixpoint in Coq

Question

I am a beginner in coq and want to prove the following theorem t1. First I used induction i and destruct j, but it got bogged down in the middle. I would like some hints for this problem.

Function f takes two arguments of nat and returns Prop (e.g., f 2 4 = x 2 ∧ x 3 ∧ x 4 ∧ x 5).

Theorem t1 shows that a head of function f can be cut and concatenated (e.g., x 3 ∧ f 4 7 ⇔ f 3 8).

Parameter x : nat -> Prop.

Fixpoint f (o i : nat) : Prop :=
 match i with
 | S O =>  x (i+o-1)
 | S i' => f o i' /\ x (i+o-1)
 | _ => True
 end.

Theorem t1 : forall i j : nat, 
    x i /\ f (S i) j <-> f i (S j).
Proof. Admitted.