proposition: Lemma all_iffLR P0 Ps : all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
proof: Proof. move=> iffPs; have PsS n: nth P0 Ps n -> nth P0 Ps n.+1. elim: n P0 Ps iffPs => [|n IHn] P0 [|P [|Q Ps]] //= [iP0P] //; first by case. by rewrite nth_nil. by case=> iPQ iffPs; apply: IHn; split=> // /iP0P. have{PsS} lePs: {homo nth P0 Ps : m n / m <= n >-> (m -> n)}. by move=> m n /subnK<-; elim: {n}(n - m) => // n IHn /IHn; apply: PsS. move=> m n P_m; have{m P_m} hP0: P0. case: m P_m => //= m /(lePs m _ (leq_maxl m (size Ps))). by rewrite nth_default ?leq_maxr. case: n =>// n; apply: lePs 0 n (leq0n n) _. by case: Ps iffPs hP0 => // P Ps []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)