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

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.

You are making your life difficult by defining things in convoluted ways. Here's how a better definition of the same thing makes the proof easy.

Fixpoint f_better n0 len : Prop :=
  match len with
  | 0 => True
  | S k => x n0 /\ f_better (S n0) k
end.

Theorem t1_better: forall n0 len,
    x n0 /\ f_better (S n0) len  f_better n0 (S len).
Proof.
  easy.
Qed.

If you really insist on using your version, we can prove that as well, but it'll be painful.

StackExchange Computer Science Q#76409, answer score: 6