fact: Definition induction_seq A (P : seq A -> Prop) : P nil -> (forall a l, P l -> P (a :: l)) -> forall l, P l := fun pn pc => fix IH l : P l := match l with nil => pn | cons a l1 => pc a l1 (IH l1) end .
imports: mathcomp(all_ssreflect)