proposition: Lemma NUMPAIR_nonzero x y : NUMPAIR x y <> 0.
proof: Proof. unfold NUMPAIR, NUMERAL, BIT1, BIT0. rewrite mul_add_distr_l, mul_1_r. assert (h: 2 ^ x <> 0). apply pow_nonzero. lia. lia. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat