proposition: Lemma all_iffP P0 Ps : all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m <-> nth P0 (P0 :: Ps) n.
proof: Proof. by move=> /all_iffLR-iffPs m n; split => /iffPs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)