proposition: Lemma nonZeroIsSucc n (p: BITS n) : p != #0 -> exists m, toNat p = m.+1.
proof: Proof. move => H. case E: (toNat p) => [| n']. + rewrite -(toNatK p) in H. by rewrite E fromNat0 eq_refl in H. + by exists n'. 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