proposition: Lemma size0nilP xs : reflect (xs = [::]) (size xs == 0).
proof: Proof. case: eqP=>X; constructor; first by move/size0nil: X. by move=>N; rewrite N in X. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)