proposition: Lemma toNatK n : cancel (@toNat n) (@fromNat n).
proof: Proof. induction n; first (move => p; apply trivialBits). + case/tupleP => b x. rewrite toNatCons/fromNat-/fromNat /= half_bit_double. rewrite IHn oddD odd_double. by case b. 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