Some ideas for tactics

[qbuzet]

In bulk:

• In #671 @QGarchery suggests to allow rewriting on hypothesis. But we can imagine allowing the tatic "simplify" too. For now, it's possible by using the tactic "simplify" before assuming hypothesis but I think that in some cases, we can want to simplify only one term.

Some syntactic sugar :

• To split a conjunction
• To simply do the modus ponens like mp thm P which would add a proof of q in the context (when thm: Prf (p => q) and P: Prf(p))

A way to manage repetitions :

• with macros
• by doing something in all the subgoals as suggested by @amelieled