Chaining tactics issues

Some thoughts I will try to address shortly, but this can start a discussion.
This follows the merging of #66.

1. There is no benefit in using sum and prop in Type instead of \/ and /\ in Prop. Depending on their background, some users can be very surprised that we build functions this way. The same apply to the second part where A, B, ... could perfectly live in Prop.
   Even with a background in type theory, this is not, imho, a case where a proof is much simpler than the hand-written term:

Definition foo (x : A * (B + C + D)) : A * B + A * C + A * D :=
  let (a, bcd) := x in
  match bcd with
  | inl bc => match bc with
              | inl b => inl (inl (a, b))
              | inr c => inl (inr (a, c))
              end
  | inr d => inr (a, d)
  end.

2. Is there an agreement on using Goal instead of Lemma foo1, Lemma foo2? I don't see a strong benefit except being able to give multiple proofs without providing new names for lemmas.
3. We should emphasize that both try and repeat break the "fail fast" principle and may make some proofs very hard to maintain.
4. Some consistency in the proof scripts style could be discussed (bullets, spaces around : or ;, spaces inside brackets, ...)
5. The fact that chaining and tactics like assumption can free us from naming explicitly assumptions could be discussed here.
6. We need to add examples with [tac1 | tac2.. | tacn].
7. The word "tactical" is not used, is it a choice?

Start by reviewing the material changed in #66 and the current chaining tactics documentation. Resolve the seven listed questions—notation, Goal usage, try/repeat guidance, style, unnamed assumptions, bracketed alternatives, and “tactical” terminology—and add the requested examples. Done means the documentation reflects an agreed scope and includes the requested examples.