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 -&gt; Prop.

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

Theorem t1 : forall i j : nat, 
    x i /\ f (S i) j &lt;-&gt; 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 =&gt; True
  | S k =&gt; x n0 /\ f_better (S n0) k
end.

Theorem t1_better: forall n0 len,
    x n0 /\ f_better (S n0) len &lt;-&gt; 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.