Question sur Coq et la tactique induction

Bonjour à tous

Récemment, j'ai décidé de m'intéresser un peu à la théorie des types et de la démonstration. Quelques vieilles dépêches y sont pour un peu, et le sujet m'avait toujours un peu intrigué.
Après quelques recherches, j'ai trouvé et commencé l'excellent Logic Foundations.
J'en suis arrivé lentement mais sûrement au chapitre sur les propositions inductives (IndProp).
Et là j'ai un petit soucis…

Lemma le_trans : forall m n o, m <= n -> n <= o -> m <= o.
Proof.
  intros m n o H1.
  generalize dependent o.

Là j'aimerais faire une induction sur H1. En regardant la définition de la relation :

Inductive le : nat -> nat -> Prop :=
  | le_n n : le n n
  | le_S n m (H : le n m) : le n (S m).
Notation "m <= n" := (le m n).

Si j'ai bien compris, lorsque l'on fait une induction sur une hypothèse, on sépare les cas en fonction du "constructeur".
Dans mon cas, je devrais avoir 2 possibilités, une pour le_n, et une pour le_S.
Je devrais donc pouvoir faire quelque chose du genre

    induction H1 as [n' | n' m' H' IH].

Seulement, il semblerait que n ne rentre pas dans le pattern.
L'écriture correcte semble être

    induction H1 as [| m' H' IH].

mais j'avoue ne pas savoir pourquoi.

En allant plus loin dans le cours, dans la partie sur les regexp, je tombe sur une autre relation inductive :

Inductive exp_match {T} : list T -> reg_exp -> Prop :=
  | MEmpty : exp_match [] EmptyStr
  | MChar x : exp_match [x] (Char x)
  | MApp s1 re1 s2 re2
             (H1 : exp_match s1 re1)
             (H2 : exp_match s2 re2) :
             exp_match (s1 ++ s2) (App re1 re2)
  | MUnionL s1 re1 re2
                (H1 : exp_match s1 re1) :
                exp_match s1 (Union re1 re2)
  | MUnionR re1 s2 re2
                (H2 : exp_match s2 re2) :
                exp_match s2 (Union re1 re2)
  | MStar0 re : exp_match [] (Star re)
  | MStarApp s1 s2 re
                 (H1 : exp_match s1 re)
                 (H2 : exp_match s2 (Star re)) :
                 exp_match (s1 ++ s2) (Star re).

et lors de l'appel à induction, on a bien tous les arguments des constructeurs qui sont mappés.

induction Hmatch
    as [| x'
        | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
        | s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
        | re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].

Du coup, je ne comprends pas pourquoi mon premier argument est sauté.
Est-ce que j'aurais loupé quelque chose ???

Mis à part ça, j'aime bien le Coq ! C'est très chronophage, et on arrive facilement à passer des heures sur une démonstration…

PS : dans la foulée, rien à voir, mais pourquoi ce calcul me renvoie un stack overflow ? La limite me semble très basse.
J'ai essayé avec un accumulateur aussi, au cas où la TCO serait prise en charge, mais on dirait que non…

Require Import Coq.Arith.Factorial.
Compute fact 10.