Transitivity of Leibniz equality

Prove manually the following theorem (already in Coq's base of theorems) : 
 forall (A:Type) (a b c:A), a = b -> b = c -> a = c.
  1. Applying explicitely eq_ind,
  2. Using Rewrite

Solution

Look at this file