fact: Definition all_iff (P0 : Prop) (Ps : seq Prop) : Prop := let fix loop (P : Prop) (Qs : seq Prop) : Prop := if Qs is Q :: Qs then all_iff_and (P -> Q) (loop Q Qs) else P -> P0 in loop P0 Ps.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)