proposition: Lemma le0B n (p : BITS n) : leB p #0 -> p = #0.
proof: Proof. rewrite leB_nat. rewrite toNat_fromNat0 => H. rewrite leqn0 in H. apply toNat_inj. by rewrite (eqP H) toNat_fromNat0. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype tuple zmodp div) ssrextra.tuple ssrextra.nat spec spec.properties operations mathcomp(ssralg)