]
qed.
+lemma exadecimal_of_nat_nat_of_exadecimal:
+ ∀b.exadecimal_of_nat (nat_of_exadecimal b) = b.
+ intro;
+ elim b;
+ reflexivity.
+qed.
+
lemma plusex_ok:
∀b1,b2,c.
match plusex b1 b2 c with
first [ reflexivity | destruct H ].
qed.
+lemma eqex_false_to_not_eq: ∀b,b'. eqex b b' = false → b ≠ b'.
+ intros 2;
+ elim b 0;
+ elim b' 0;
+ simplify;
+ intro;
+ try (destruct H);
+ intro K;
+ destruct K.
+qed.
+
(*
lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b.
intros;