set "baseuri" "cic:/matita/assembly/exadecimal/".
-include "extra.ma".
+include "assembly/extra.ma".
inductive exadecimal : Type ≝
x0: exadecimal
change in ⊢ (? ? ? (? (? % ?))) with (n16 \mod 16);
rewrite < mod_mod;
[ apply H;
- autobatch
+ unfold lt;
+ autobatch.
| autobatch
]
qed.
match plusex b1 b2 c with
[ couple r c' ⇒ b1 + b2 + nat_of_bool c = nat_of_exadecimal r + nat_of_bool c' * 16 ].
intros;
- elim c;
- elim b1;
- elim b2;
- normalize;
- reflexivity.
+ elim b1; (elim b2; (elim c; normalize; reflexivity)).
qed.
definition xpred ≝
intros;
rewrite > exadecimal_of_nat_mod;
rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %);
-*)
\ No newline at end of file
+*)