[ x0 ⇒ 0 | x1 ⇒ 1 | x2 ⇒ 2 | x3 ⇒ 3 | x4 ⇒ 4 | x5 ⇒ 5 | x6 ⇒ 6 | x7 ⇒ 7
| x8 ⇒ 8 | x9 ⇒ 9 | xA ⇒ 10 | xB ⇒ 11 | xC ⇒ 12 | xD ⇒ 13 | xE ⇒ 14 | xF ⇒ 15 ].
-coercion cic:/matita/freescale/exadecim/nat_of_exadecim.con.
+coercion nat_of_exadecim.
(* naturali → esadecimali *)
let rec exadecim_of_nat n ≝
intro;
elim e;
simplify;
- autobatch depth=17.
+ unfold;autobatch depth=17 size=20.
qed.
lemma exadecim_of_nat_mod:
rewrite < mod_mod;
[ apply H;
unfold lt;
- autobatch.
+ autobatch depth=20 size=20.
| autobatch
]
qed.