proposition: Lemma empty_finType_nil (T : finType) : (#|T| = 0) -> forall c : seq T, c = [::].
proof: Proof. move/card0_eq => T0; by case=> // h; move: (T0 h); rewrite !inE. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext