Is there a tactic to reorder the display of hypothesis within a Coq proof. Very often while using induction (the hypothesis are very long) and I would like to print all definitions at the top and all other equations together.
Just to clarify, Coq does come with tactics to reorder hypotheses. These are listed in the documentation
Namely you will be interested in
move h before h'.
move h after h'.
move h at top.
move h at bottom.
The documentation comes with useful examples, but the names should be self-explanatory.