proposition: Lemma rtrans_ind (P : T -> Prop) x : P x -> (forall y z, P y -> z \in rule y -> P z) -> forall t, rtrans x t -> P t.
proof: Proof. Proof using. move=> Hx IHr t /rtransP[l]. elim: l x Hx t => [|l0 l IHl] x Hx t /= Hpath -> //=. move: Hpath => /andP[Hl0 Hpath]. by apply: (@IHl l0); first exact: (@IHr x). Qed.
imports: HB(structures) mathcomp(all_ssreflect) Recdef permcomp permuted multinomial vectNK