fact: Fixpoint pred_prodn (T:Type) (P:T -> Prop) (n:nat) : prodn T n -> Prop := match n with | 0 => fun _ => True | S _ => fun Es => let (hd,tl) := Es in P hd /\ pred_prodn P tl end.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)