proposition: Lemma trivialBits (p q: BITS 0) : p = q.
proof: Proof. by rewrite (tuple0 p) (tuple0 q). Qed.
imports: Coq(ZArith.ZArith) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple div zmodp ssralg) ssrextra.nat ssrextra.tuple spec.spec