(*
lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
intros;
rewrite > exadecimal_of_nat_mod;
rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
(*
lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
intros;
rewrite > exadecimal_of_nat_mod;
rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);